---

Step * 1 of Lemma monad-from_wf

.....implicit subterm..... 
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)
⊢ TypeCat ∈ SmallCategory'
BY
{ Auto }

---

Latex:

---

Latex:
.....implicit  subterm..... 
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{}  TypeCat  \mmember{}  SmallCategory'


By

---

Latex:
Auto

---

Home Index