---

Step * 4 of Lemma monad-from_wf

.....subterm..... T:t
3: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,z. (M-bind(Mnd) z (λx.x))
  ∈ nat-trans(TypeCat;TypeCat;functor-comp(functor(ob(T) = M-map(Mnd) T;
                                                   arrow(X,Y,f) = λz.(M-bind(Mnd) z (λx.(M-return(Mnd) (f x)))));
                                           functor(ob(T) = M-map(Mnd) T;
                                                   arrow(X,Y,f) = λz.(M-bind(Mnd) z 
                                                                      (λx.(M-return(Mnd) 
                                                                           (f x))))));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 compose`` 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)
⊢ λx,z. (M-bind(Mnd) z (λx.x)) ∈ {trans:A:Type ⟶ (M-map(Mnd) (M-map(Mnd) A)) ⟶ (M-map(Mnd) A)| 
                              ∀A,B:Type. ∀g:A ⟶ B.
                                ((λx.(M-bind(Mnd) (trans A x) (λx.(M-return(Mnd) (g x)))))
                                = (λx.(trans B 
                                       (M-bind(Mnd) x (λx.(M-return(Mnd) (M-bind(Mnd) x (λx.(M-return(Mnd) (g x)))))))))
                                ∈ ((M-map(Mnd) (M-map(Mnd) A)) ⟶ (M-map(Mnd) B)))} 

---

Latex:

---

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


By

---

Latex:
RepUR  ``type-cat  mk-cat  nat-trans  functor-comp  compose``  0

---

Home Index