---

Step * 3 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)
⊢ λx.M-return(Mnd) ∈ nat-trans(TypeCat;TypeCat;1;functor(ob(T) = M-map(Mnd) T;
                                                         arrow(X,Y,f) = λz.(M-bind(Mnd) z (λx.(M-return(Mnd) (f x))))))
BY
{ (RepUR ``type-cat mk-cat nat-trans functor-comp id_functor`` 0 THEN MemTypeCD THEN 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. A : Type
4. B : Type
5. g : A ⟶ B
⊢ ((λz.(M-bind(Mnd) z (λx.(M-return(Mnd) (g x))))) o ((λx.M-return(Mnd)) A))
= (((λx.M-return(Mnd)) B) o g)
∈ (A ⟶ (M-map(Mnd) B))

---

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)
\mvdash{}  \mlambda{}x.M-return(Mnd)  \mmember{}  nat-trans(TypeCat;TypeCat;1;functor(ob(T)  =  M-map(Mnd)  T;
                                                                                                                  arrow(X,Y,f)  =  \mlambda{}z.(M-bind(Mnd)  z 
                                                                                                                                                        (\mlambda{}x.(M-return(Mnd) 
                                                                                                                                                                  (f  x))))))


By

---

Latex:
(RepUR  ``type-cat  mk-cat  nat-trans  functor-comp  id\_functor``  0  THEN  MemTypeCD  THEN  Auto)

---

Home Index