---

Step * 2 3 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:cat-ob(TypeCat)
    ((λz.(M-bind(Mnd) z (λx@0.(M-return(Mnd) (cat-id(TypeCat) X x@0)))))
    = (cat-id(TypeCat) (M-map(Mnd) X))
    ∈ (cat-arrow(TypeCat) (M-map(Mnd) X) (M-map(Mnd) X)))
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. x : M-map(Mnd) X
⊢ (M-bind(Mnd) x (λx@0.(M-return(Mnd) x@0))) = x ∈ (M-map(Mnd) X)

---

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:cat-ob(TypeCat)
        ((\mlambda{}z.(M-bind(Mnd)  z  (\mlambda{}x@0.(M-return(Mnd)  (cat-id(TypeCat)  X  x@0)))))
        =  (cat-id(TypeCat)  (M-map(Mnd)  X)))


By

---

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

---

Home Index