Signed-off-by: Jim Pryor <profjim@jimpryor.net>
To have a category, the elements and morphisms have to satisfy some constraints:
<pre>
To have a category, the elements and morphisms have to satisfy some constraints:
<pre>
- (i) the class of morphisms has to be closed under composition: where f:C1→C2 and g:C2→C3, g º f is also a morphism of the category, which maps C1→C3.
+ (i) the class of morphisms has to be closed under composition: where f:C1→C2 and g:C2→C3, g ∘ f is also a morphism of the category, which maps C1→C3.
(ii) composition of morphisms has to be associative
(ii) composition of morphisms has to be associative
- (iii) every element E of the category has to have an identity morphism 1<sub>E</sub>, which is such that for every morphism f:C1→C2: 1<sub>C2</sub> o f = f = f o 1<sub>C1</sub>
+ (iii) every element E of the category has to have an identity morphism 1<sub>E</sub>, which is such that for every morphism f:C1→C2: 1<sub>C2</sub> ∘ f = f = f ∘ 1<sub>C1</sub>
</pre>
These parallel the constraints for monoids. Note that there can be multiple distinct morphisms between an element `E` and itself; they need not all be identity morphisms. Indeed from (iii) it follows that each element can have only a single identity morphism.
</pre>
These parallel the constraints for monoids. Note that there can be multiple distinct morphisms between an element `E` and itself; they need not all be identity morphisms. Indeed from (iii) it follows that each element can have only a single identity morphism.
(i) associate with every element C1 of <b>C</b> an element F(C1) of <b>D</b>
(ii) associate with every morphism f:C1→C2 of <b>C</b> a morphism F(f):F(C1)→F(C2) of <b>D</b>
(iii) "preserve identity", that is, for every element C1 of <b>C</b>: F of C1's identity morphism in <b>C</b> must be the identity morphism of F(C1) in <b>D</b>: F(1<sub>C1</sub>) = 1<sub>F(C1)</sub>.
(i) associate with every element C1 of <b>C</b> an element F(C1) of <b>D</b>
(ii) associate with every morphism f:C1→C2 of <b>C</b> a morphism F(f):F(C1)→F(C2) of <b>D</b>
(iii) "preserve identity", that is, for every element C1 of <b>C</b>: F of C1's identity morphism in <b>C</b> must be the identity morphism of F(C1) in <b>D</b>: F(1<sub>C1</sub>) = 1<sub>F(C1)</sub>.
- (iv) "distribute over composition", that is for any morphisms f and g in <b>C</b>: F(g o f) = F(g) o F(f)
+ (iv) "distribute over composition", that is for any morphisms f and g in <b>C</b>: F(g ∘ f) = F(g) ∘ F(f)
</pre>
A functor that maps a category to itself is called an **endofunctor**. The (endo)functor that maps every element and morphism of <b>C</b> to itself is denoted `1C`.
</pre>
A functor that maps a category to itself is called an **endofunctor**. The (endo)functor that maps every element and morphism of <b>C</b> to itself is denoted `1C`.
Where `G` and `H` are functors from category <b>C</b> to category <b>D</b>, a natural transformation η between `G` and `H` is a family of morphisms η[C1]:G(C1)→H(C1)` in <b>D</b> for each element `C1` of <b>C</b>. That is, η[C1]` has as source `C1`'s image under `G` in <b>D</b>, and as target `C1`'s image under `H` in <b>D</b>. The morphisms in this family must also satisfy the constraint:
Where `G` and `H` are functors from category <b>C</b> to category <b>D</b>, a natural transformation η between `G` and `H` is a family of morphisms η[C1]:G(C1)→H(C1)` in <b>D</b> for each element `C1` of <b>C</b>. That is, η[C1]` has as source `C1`'s image under `G` in <b>D</b>, and as target `C1`'s image under `H` in <b>D</b>. The morphisms in this family must also satisfy the constraint:
- for every morphism f:C1→C2 in <b>C</b>: η[C2] o G(f) = H(f) o η[C1]
+ for every morphism f:C1→C2 in <b>C</b>: η[C2] ∘ G(f) = H(f) ∘ η[C1]
That is, the morphism via `G(f)` from `G(C1)` to `G(C2)`, and then via η[C2]` to `H(C2)`, is identical to the morphism from `G(C1)` via η[C1]` to `H(C1)`, and then via `H(f)` from `H(C1)` to `H(C2)`.
That is, the morphism via `G(f)` from `G(C1)` to `G(C2)`, and then via η[C2]` to `H(C2)`, is identical to the morphism from `G(C1)` via η[C1]` to `H(C1)`, and then via `H(f)` from `H(C1)` to `H(C2)`.
`(φ -v- η)` is a natural transformation from `G` to `J`; this is known as a "vertical composition". We will rely later on this, where `f:C1→C2`:
`(φ -v- η)` is a natural transformation from `G` to `J`; this is known as a "vertical composition". We will rely later on this, where `f:C1→C2`:
- φ[C2] o H(f) o η[C1] = φ[C2] o H(f) o η[C1]
+ φ[C2] ∘ H(f) ∘ η[C1] = φ[C2] ∘ H(f) ∘ η[C1]
by naturalness of φ, is:
by naturalness of φ, is:
- φ[C2] o H(f) o η[C1] = J(f) o φ[C1] o η[C1]
+ φ[C2] ∘ H(f) ∘ η[C1] = J(f) ∘ φ[C1] ∘ η[C1]
by naturalness of η, is:
by naturalness of η, is:
- φ[C2] o η[C2] o G(f) = J(f) o φ[C1] o η[C1]
+ φ[C2] ∘ η[C2] ∘ G(f) = J(f) ∘ φ[C1] ∘ η[C1]
-Hence, we can define `(φ -v- η)[x]` as: φ[x] o η[x]` and rely on it to satisfy the constraints for a natural transformation from `G` to `J`:
+Hence, we can define `(φ -v- η)[x]` as: φ[x] ∘ η[x]` and rely on it to satisfy the constraints for a natural transformation from `G` to `J`:
- (φ -v- η)[C2] o G(f) = J(f) o (φ -v- η)[C1]
+ (φ -v- η)[C2] ∘ G(f) = J(f) ∘ (φ -v- η)[C1]
An observation we'll rely on later: given the definitions of vertical composition and of how natural transformations compose with functors, it follows that:
An observation we'll rely on later: given the definitions of vertical composition and of how natural transformations compose with functors, it follows that:
`(ψ -h- η)` is natural transformation from the (composite) functor `KG` to the (composite) functor `LH`; this is known as a "horizontal composition." It's trickier to define, but we won't be using it here. For reference:
`(ψ -h- η)` is natural transformation from the (composite) functor `KG` to the (composite) functor `LH`; this is known as a "horizontal composition." It's trickier to define, but we won't be using it here. For reference:
- (φ -h- η)[C1] = L(η[C1]) o ψ[G(C1)]
- = ψ[H(C1)] o K(η[C1])
+ (φ -h- η)[C1] = L(η[C1]) ∘ ψ[G(C1)]
+ = ψ[H(C1)] ∘ K(η[C1])
Horizontal composition is also associative, and has the same identity as vertical composition.
Horizontal composition is also associative, and has the same identity as vertical composition.
In category theory, the monad laws are usually stated in terms of `unit` and `join` instead of `unit` and `<=<`.
(*
In category theory, the monad laws are usually stated in terms of `unit` and `join` instead of `unit` and `<=<`.
(*
- P2. every element C1 of a category <b>C</b> has an identity morphism 1<sub>C1</sub> such that for every morphism f:C1→C2 in <b>C</b>: 1<sub>C2</sub> o f = f = f o 1<sub>C1</sub>.
+ P2. every element C1 of a category <b>C</b> has an identity morphism 1<sub>C1</sub> such that for every morphism f:C1→C2 in <b>C</b>: 1<sub>C2</sub> ∘ f = f = f ∘ 1<sub>C1</sub>.
P3. functors "preserve identity", that is for every element C1 in F's source category: F(1<sub>C1</sub>) = 1<sub>F(C1)</sub>.
*)
Let's remind ourselves of some principles:
* composition of morphisms, functors, and natural compositions is associative
P3. functors "preserve identity", that is for every element C1 in F's source category: F(1<sub>C1</sub>) = 1<sub>F(C1)</sub>.
*)
Let's remind ourselves of some principles:
* composition of morphisms, functors, and natural compositions is associative
- * functors "distribute over composition", that is for any morphisms f and g in F's source category: F(g o f) = F(g) o F(f)
- * if η is a natural transformation from F to G, then for every f:C1→C2 in F and G's source category <b>C</b>: η[C2] o F(f) = G(f) o η[C1].
+ * functors "distribute over composition", that is for any morphisms f and g in F's source category: F(g ∘ f) = F(g) ∘ F(f)
+ * if η is a natural transformation from F to G, then for every f:C1→C2 in F and G's source category <b>C</b>: η[C2] ∘ F(f) = G(f) ∘ η[C1].
Let's use the definitions of naturalness, and of composition of natural transformations, to establish two lemmas.
Let's use the definitions of naturalness, and of composition of natural transformations, to establish two lemmas.
Recall that join is a natural transformation from the (composite) functor MM to M. So for elements C1 in <b>C</b>, join[C1] will be a morphism from MM(C1) to M(C1). And for any morphism f:a→b in <b>C</b>:
Recall that join is a natural transformation from the (composite) functor MM to M. So for elements C1 in <b>C</b>, join[C1] will be a morphism from MM(C1) to M(C1). And for any morphism f:a→b in <b>C</b>:
- (1) join[b] o MM(f) = M(f) o join[a]
+ (1) join[b] ∘ MM(f) = M(f) ∘ join[a]
Next, consider the composite transformation ((join MQ') -v- (MM q)).
q is a transformation from Q to MQ', and assigns elements C1 in <b>C</b> a morphism q*: Q(C1) → MQ'(C1). (MM q) is a transformation that instead assigns C1 the morphism MM(q*).
(join MQ') is a transformation from MMMQ' to MMQ' that assigns C1 the morphism join[MQ'(C1)].
Composing them:
Next, consider the composite transformation ((join MQ') -v- (MM q)).
q is a transformation from Q to MQ', and assigns elements C1 in <b>C</b> a morphism q*: Q(C1) → MQ'(C1). (MM q) is a transformation that instead assigns C1 the morphism MM(q*).
(join MQ') is a transformation from MMMQ' to MMQ' that assigns C1 the morphism join[MQ'(C1)].
Composing them:
- (2) ((join MQ') -v- (MM q)) assigns to C1 the morphism join[MQ'(C1)] o MM(q*).
+ (2) ((join MQ') -v- (MM q)) assigns to C1 the morphism join[MQ'(C1)] ∘ MM(q*).
Next, consider the composite transformation ((M q) -v- (join Q)).
Next, consider the composite transformation ((M q) -v- (join Q)).
- (3) This assigns to C1 the morphism M(q*) o join[Q(C1)].
+ (3) This assigns to C1 the morphism M(q*) ∘ join[Q(C1)].
So for every element C1 of <b>C</b>:
((join MQ') -v- (MM q))[C1], by (2) is:
So for every element C1 of <b>C</b>:
((join MQ') -v- (MM q))[C1], by (2) is:
- join[MQ'(C1)] o MM(q*), which by (1), with f=q*: Q(C1)→MQ'(C1) is:
- M(q*) o join[Q(C1)], which by 3 is:
+ join[MQ'(C1)] ∘ MM(q*), which by (1), with f=q*: Q(C1)→MQ'(C1) is:
+ M(q*) ∘ join[Q(C1)], which by 3 is:
((M q) -v- (join Q))[C1]
So our (lemma 1) is: ((join MQ') -v- (MM q)) = ((M q) -v- (join Q)), where q is a transformation from Q to MQ'.
Next recall that unit is a natural transformation from 1C to M. So for elements C1 in <b>C</b>, unit[C1] will be a morphism from C1 to M(C1). And for any morphism f:a→b in <b>C</b>:
((M q) -v- (join Q))[C1]
So our (lemma 1) is: ((join MQ') -v- (MM q)) = ((M q) -v- (join Q)), where q is a transformation from Q to MQ'.
Next recall that unit is a natural transformation from 1C to M. So for elements C1 in <b>C</b>, unit[C1] will be a morphism from C1 to M(C1). And for any morphism f:a→b in <b>C</b>:
- (4) unit[b] o f = M(f) o unit[a]
+ (4) unit[b] ∘ f = M(f) ∘ unit[a]
-Next consider the composite transformation ((M q) -v- (unit Q)). (5) This assigns to C1 the morphism M(q*) o unit[Q(C1)].
+Next consider the composite transformation ((M q) -v- (unit Q)). (5) This assigns to C1 the morphism M(q*) ∘ unit[Q(C1)].
-Next consider the composite transformation ((unit MQ') -v- q). (6) This assigns to C1 the morphism unit[MQ'(C1)] o q*.
+Next consider the composite transformation ((unit MQ') -v- q). (6) This assigns to C1 the morphism unit[MQ'(C1)] ∘ q*.
So for every element C1 of <b>C</b>:
((M q) -v- (unit Q))[C1], by (5) =
So for every element C1 of <b>C</b>:
((M q) -v- (unit Q))[C1], by (5) =
- M(q*) o unit[Q(C1)], which by (4), with f=q*: Q(C1)→MQ'(C1) is:
- unit[MQ'(C1)] o q*, which by (6) =
+ M(q*) ∘ unit[Q(C1)], which by (4), with f=q*: Q(C1)→MQ'(C1) is:
+ unit[MQ'(C1)] ∘ q*, which by (6) =
((unit MQ') -v- q)[C1]
So our lemma (2) is: (((M q) -v- (unit Q)) = ((unit MQ') -v- q)), where q is a transformation from Q to MQ'.
((unit MQ') -v- q)[C1]
So our lemma (2) is: (((M q) -v- (unit Q)) = ((unit MQ') -v- q)), where q is a transformation from Q to MQ'.
A natural transformation t assigns to each type C1 in <b>C</b> a morphism t[C1]: C1→M(C1) such that, for every f:C1→C2:
A natural transformation t assigns to each type C1 in <b>C</b> a morphism t[C1]: C1→M(C1) such that, for every f:C1→C2:
- t[C2] o f = M(f) o t[C1]
+ t[C2] ∘ f = M(f) ∘ t[C1]
The composite morphisms said here to be identical are morphisms from the type C1 to the type M(C2).
The composite morphisms said here to be identical are morphisms from the type C1 to the type M(C2).