---

Step * 2 1 1 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)
3. X : cat-ob(TypeCat)
4. Y : cat-ob(TypeCat)
5. f : cat-arrow(TypeCat) X Y
⊢ λz.(M-bind(Mnd) z (λx.(M-return(Mnd) (f x)))) ∈ (M-map(Mnd) X) ⟶ (M-map(Mnd) Y)
BY
{ (Assert λx.(M-return(Mnd) (f x)) ∈ X ⟶ (M-map(Mnd) Y) BY
         Auto) }

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 : cat-ob(TypeCat)
4. Y : cat-ob(TypeCat)
5. f : cat-arrow(TypeCat) X Y
6. λx.(M-return(Mnd) (f x)) ∈ X ⟶ (M-map(Mnd) Y)
⊢ λz.(M-bind(Mnd) z (λx.(M-return(Mnd) (f x)))) ∈ (M-map(Mnd) X) ⟶ (M-map(Mnd) Y)

---

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)
3.  X  :  cat-ob(TypeCat)
4.  Y  :  cat-ob(TypeCat)
5.  f  :  cat-arrow(TypeCat)  X  Y
\mvdash{}  \mlambda{}z.(M-bind(Mnd)  z  (\mlambda{}x.(M-return(Mnd)  (f  x))))  \mmember{}  (M-map(Mnd)  X)  {}\mrightarrow{}  (M-map(Mnd)  Y)


By

---

Latex:
(Assert  \mlambda{}x.(M-return(Mnd)  (f  x))  \mmember{}  X  {}\mrightarrow{}  (M-map(Mnd)  Y)  BY
              Auto)

---

Home Index