cat theory tweaks
[lambda.git] / advanced_topics / monads_in_category_theory.mdwn
index 078bec2..29b6feb 100644 (file)
@@ -104,60 +104,77 @@ Natural Transformation
 ----------------------
 So categories include elements and morphisms. Functors consist of mappings from the elements and morphisms of one category to those of another (or the same) category. **Natural transformations** are a third level of mappings, from one functor to another.
 
 ----------------------
 So categories include elements and morphisms. Functors consist of mappings from the elements and morphisms of one category to those of another (or the same) category. **Natural transformations** are a third level of mappings, from one functor to another.
 
-Where `G` and `H` are functors from category <b>C</b> to category <b>D</b>, a natural transformation &eta; between `G` and `H` is a family of morphisms &eta;[C1]:G(C1)&rarr;H(C1)` in <b>D</b> for each element `C1` of <b>C</b>. That is, &eta;[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 &eta; between `G` and `H` is a family of morphisms <code>&eta;[C1]:G(C1)&rarr;H(C1)</code> in <b>D</b> for each element `C1` of <b>C</b>. That is, <code>&eta;[C1]</code> 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&rarr;C2 in <b>C</b>: &eta;[C2] &#8728; G(f) = H(f) &#8728; &eta;[C1]
+<pre>
+       for every morphism f:C1&rarr;C2 in <b>C</b>:
+       &eta;[C2] &#8728; G(f) = H(f) &#8728; &eta;[C1]
+</pre>
 
 
-That is, the morphism via `G(f)` from `G(C1)` to `G(C2)`, and then via &eta;[C2]` to `H(C2)`, is identical to the morphism from `G(C1)` via &eta;[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 <code>&eta;[C2]</code> to `H(C2)`, is identical to the morphism from `G(C1)` via <code>&eta;[C1]</code> to `H(C1)`, and then via `H(f)` from `H(C1)` to `H(C2)`.
 
 
 How natural transformations compose:
 
 Consider four categories <b>B</b>, <b>C</b>, <b>D</b>, and <b>E</b>. Let `F` be a functor from <b>B</b> to <b>C</b>; `G`, `H`, and `J` be functors from <b>C</b> to <b>D</b>; and `K` and `L` be functors from <b>D</b> to <b>E</b>. Let &eta; be a natural transformation from `G` to `H`; &phi; be a natural transformation from `H` to `J`; and &psi; be a natural transformation from `K` to `L`. Pictorally:
 
 
 
 How natural transformations compose:
 
 Consider four categories <b>B</b>, <b>C</b>, <b>D</b>, and <b>E</b>. Let `F` be a functor from <b>B</b> to <b>C</b>; `G`, `H`, and `J` be functors from <b>C</b> to <b>D</b>; and `K` and `L` be functors from <b>D</b> to <b>E</b>. Let &eta; be a natural transformation from `G` to `H`; &phi; be a natural transformation from `H` to `J`; and &psi; be a natural transformation from `K` to `L`. Pictorally:
 
+<pre>
        - <b>B</b> -+ +--- <b>C</b> --+ +---- <b>D</b> -----+ +-- <b>E</b> --
                 | |        | |            | |
        - <b>B</b> -+ +--- <b>C</b> --+ +---- <b>D</b> -----+ +-- <b>E</b> --
                 | |        | |            | |
-        F: -----&rarr; G: -----&rarr;     K: -----&rarr;
-                | |        | |  | &eta;     | |  | &psi;
+        F: ------> G: ------>     K: ------>
+                | |        | |  | &eta;       | |  | &psi;
                 | |        | |  v         | |  v
                 | |        | |  v         | |  v
-                | |    H: -----&rarr;     L: -----&rarr;
-                | |        | |  | &phi;     | |
+                | |    H: ------>     L: ------>
+                | |        | |  | &phi;       | |
                 | |        | |  v         | |
                 | |        | |  v         | |
-                | |    J: -----&rarr;         | |
+                | |    J: ------>         | |
        -----+ +--------+ +------------+ +-------
        -----+ +--------+ +------------+ +-------
+</pre>
 
 
-Then `(&eta; F)` is a natural transformation from the (composite) functor `GF` to the composite functor `HF`, such that where `b1` is an element of category <b>B</b>, `(&eta; F)[b1] = &eta;[F(b1)]`---that is, the morphism in <b>D</b> that &eta; assigns to the element `F(b1)` of <b>C</b>.
+Then <code>(&eta; F)</code> is a natural transformation from the (composite) functor `GF` to the composite functor `HF`, such that where `B1` is an element of category <b>B</b>, <code>(&eta; F)[B1] = &eta;[F(B1)]</code>---that is, the morphism in <b>D</b> that <code>&eta;</code> assigns to the element `F(B1)` of <b>C</b>.
 
 
-And `(K &eta;)` is a natural transformation from the (composite) functor `KG` to the (composite) functor `KH`, such that where `C1` is an element of category <b>C</b>, `(K &eta;)[C1] = K(&eta;[C1])`---that is, the morphism in <b>E</b> that `K` assigns to the morphism &eta;[C1]` of <b>D</b>.
+And <code>(K &eta;)</code> is a natural transformation from the (composite) functor `KG` to the (composite) functor `KH`, such that where `C1` is an element of category <b>C</b>, <code>(K &eta;)[C1] = K(&eta;[C1])</code>---that is, the morphism in <b>E</b> that `K` assigns to the morphism <code>&eta;[C1]</code> of <b>D</b>.
 
 
 
 
-`(&phi; -v- &eta;)` is a natural transformation from `G` to `J`; this is known as a "vertical composition". We will rely later on this, where `f:C1&rarr;C2`:
+<code>(&phi; -v- &eta;)</code> is a natural transformation from `G` to `J`; this is known as a "vertical composition". We will rely later on this, where <code>f:C1&rarr;C2</code>:
 
 
+<pre>
        &phi;[C2] &#8728; H(f) &#8728; &eta;[C1] = &phi;[C2] &#8728; H(f) &#8728; &eta;[C1]
        &phi;[C2] &#8728; H(f) &#8728; &eta;[C1] = &phi;[C2] &#8728; H(f) &#8728; &eta;[C1]
+</pre>
 
 
-by naturalness of &phi;, is:
+by naturalness of <code>&phi;</code>, is:
 
 
+<pre>
        &phi;[C2] &#8728; H(f) &#8728; &eta;[C1] = J(f) &#8728; &phi;[C1] &#8728; &eta;[C1]
        &phi;[C2] &#8728; H(f) &#8728; &eta;[C1] = J(f) &#8728; &phi;[C1] &#8728; &eta;[C1]
+</pre>
 
 
-by naturalness of &eta;, is:
+by naturalness of <code>&eta;</code>, is:
 
 
+<pre>
        &phi;[C2] &#8728; &eta;[C2] &#8728; G(f) = J(f) &#8728; &phi;[C1] &#8728; &eta;[C1]
        &phi;[C2] &#8728; &eta;[C2] &#8728; G(f) = J(f) &#8728; &phi;[C1] &#8728; &eta;[C1]
+</pre>
 
 
-Hence, we can define `(&phi; -v- &eta;)[x]` as: &phi;[x] &#8728; &eta;[x]` and rely on it to satisfy the constraints for a natural transformation from `G` to `J`:
+Hence, we can define <code>(&phi; -v- &eta;)[\_]</code> as: <code>&phi;[\_] &#8728; &eta;[\_]</code> and rely on it to satisfy the constraints for a natural transformation from `G` to `J`:
 
 
+<pre>
        (&phi; -v- &eta;)[C2] &#8728; G(f) = J(f) &#8728; (&phi; -v- &eta;)[C1]
        (&phi; -v- &eta;)[C2] &#8728; G(f) = J(f) &#8728; (&phi; -v- &eta;)[C1]
+</pre>
 
 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:
 
+<pre>
        ((&phi; -v- &eta;) F) = ((&phi; F) -v- (&eta; F))
        ((&phi; -v- &eta;) F) = ((&phi; F) -v- (&eta; F))
+</pre>
 
 I'll assert without proving that vertical composition is associative and has an identity, which we'll call "the identity transformation."
 
 
 
 I'll assert without proving that vertical composition is associative and has an identity, which we'll call "the identity transformation."
 
 
-`(&psi; -h- &eta;)` 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:
+<code>(&psi; -h- &eta;)</code> 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:
 
 
+<pre>
        (&phi; -h- &eta;)[C1]  =  L(&eta;[C1]) &#8728; &psi;[G(C1)]
        (&phi; -h- &eta;)[C1]  =  L(&eta;[C1]) &#8728; &psi;[G(C1)]
-                                          =  &psi;[H(C1)] &#8728; K(&eta;[C1])
+                                 =  &psi;[H(C1)] &#8728; K(&eta;[C1])
+</pre>
 
 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.