---

Step * 2 2 of Lemma monad-from_wf


1. Mnd : Monad
2. λx,z. (M-bind(Mnd) z (λx.x)) ∈ A:Type ⟶ (M-map(Mnd) (M-map(Mnd) A)) ⟶ (M-map(Mnd) A)
⊢ ∀X,Y,z:cat-ob(TypeCat). ∀f:cat-arrow(TypeCat) X Y. ∀g:cat-arrow(TypeCat) Y z.
    ((λz@0.(M-bind(Mnd) z@0 (λx@0.(M-return(Mnd) (cat-comp(TypeCat) X Y z f g x@0)))))
    = (cat-comp(TypeCat) (M-map(Mnd) X) (M-map(Mnd) Y) (M-map(Mnd) z) (λz.(M-bind(Mnd) z (λx.(M-return(Mnd) (f x))))) 
       (λz.(M-bind(Mnd) z (λx.(M-return(Mnd) (g x))))))
    ∈ (cat-arrow(TypeCat) (M-map(Mnd) X) (M-map(Mnd) z)))
BY
{ (RepUR ``type-cat compose`` 0 THEN Auto THEN (FunExt THENA Auto) THEN Reduce 0) }

1
1. Mnd : Monad
2. λx,z. (M-bind(Mnd) z (λx.x)) ∈ A:Type ⟶ (M-map(Mnd) (M-map(Mnd) A)) ⟶ (M-map(Mnd) A)
3. X : Type
4. Y : Type
5. z : Type
6. f : X ⟶ Y
7. g : Y ⟶ z
8. x : M-map(Mnd) X
⊢ (M-bind(Mnd) x (λx@0.(M-return(Mnd) (g (f x@0)))))
= (M-bind(Mnd) (M-bind(Mnd) x (λx.(M-return(Mnd) (f x)))) (λx.(M-return(Mnd) (g x))))
∈ (M-map(Mnd) z)

---

Latex:

---

Latex:

1.  Mnd  :  Monad
2.  \mlambda{}x,z.  (M-bind(Mnd)  z  (\mlambda{}x.x))  \mmember{}  A:Type  {}\mrightarrow{}  (M-map(Mnd)  (M-map(Mnd)  A))  {}\mrightarrow{}  (M-map(Mnd)  A)
\mvdash{}  \mforall{}X,Y,z:cat-ob(TypeCat).  \mforall{}f:cat-arrow(TypeCat)  X  Y.  \mforall{}g:cat-arrow(TypeCat)  Y  z.
        ((\mlambda{}z@0.(M-bind(Mnd)  z@0  (\mlambda{}x@0.(M-return(Mnd)  (cat-comp(TypeCat)  X  Y  z  f  g  x@0)))))
        =  (cat-comp(TypeCat)  (M-map(Mnd)  X)  (M-map(Mnd)  Y)  (M-map(Mnd)  z) 
              (\mlambda{}z.(M-bind(Mnd)  z  (\mlambda{}x.(M-return(Mnd)  (f  x))))) 
              (\mlambda{}z.(M-bind(Mnd)  z  (\mlambda{}x.(M-return(Mnd)  (g  x)))))))


By

---

Latex:
(RepUR  ``type-cat  compose``  0  THEN  Auto  THEN  (FunExt  THENA  Auto)  THEN  Reduce  0)

---

Home Index