Murat Kasimov

More about me

Я language (β)

/Я language (β)/Glossary/Factoring/

In general, when it's said "factoring through" it means that some morphish took an implicit roundabout which depends on exact object and unique morphism from/into it.

As an example, let's take a look at ho operator where both categories and functor are Arrow:

> `ho` : i `AR` a `AR_____` a `AR` o `AR____` i `AR` o

In this case you can use this operator as left-to-right Arrow composition:

> x : Latin `AR` Glyph > xx : Glyph `AR` Digit > x `ho` xx : Latin `AR` Digit

Sometimes we want to ignore Arrow output and replace it with some value instead, we have an operator for it - hu :

> `hu` : i `AR` a `AR_____` o `AR____` i `AR` o

This hu operator actually works similarly to ho - also maps covariantly on 2/2 argument - but factoring through Unit object.

Let's focus on source morphisms for both ho and hu operators since it's the only difference between them:

> source ( `ho` ) : a `AR` o > source ( `hu` ) : o

We can use the fact that value can be transformed into a dumb Arrow:

: Supertype ( Unit `AR` o ) ~ o > wrap : o `AR____` Unit `AR` o

Now watch closely at my hands - we are going to map terminal morphism contravariantly on 1/2 argument to this source morphism:

> source : Unit `AR` o > terminal : a `AR` Unit > source `ha` terminal : a `AR` o

And this is exactly source morphism of ho operator!