---

Step * 2 1 of Lemma monad-from_wf

.....subterm..... T:t
2:n
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)))) ∈ cat-arrow(TypeCat) (M-map(Mnd) X) (M-map(Mnd) Y)
BY
{ RepUR ``type-cat`` 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 : 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)

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
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{}  cat-arrow(TypeCat)  (M-map(Mnd)  X)  (M-map(Mnd)  Y)


By

---

Latex:
RepUR  ``type-cat``  0

---

Home Index