---

Step * 2 of Lemma monad-from_wf

.....subterm..... T:t
1: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)
⊢ functor(ob(T) = M-map(Mnd) T;
          arrow(X,Y,f) = λz.(M-bind(Mnd) z (λx.(M-return(Mnd) (f x))))) ∈ Functor(TypeCat;TypeCat)
BY
{ (MemCD THEN Try (QuickAuto)) }

1
.....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)

2
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,Y,z:cat-ob(TypeCat). ∀f:cat-arrow(TypeCat) X Y. ∀g:cat-arrow(TypeCat) Y z.
    ((λz@0.(M-bind(Mnd) z@0 (λx@0.(M-return(Mnd) (cat-comp(TypeCat) X Y z f g x@0)))))
    = (cat-comp(TypeCat) (M-map(Mnd) X) (M-map(Mnd) Y) (M-map(Mnd) z) (λz.(M-bind(Mnd) z (λx.(M-return(Mnd) (f x))))) 
       (λz.(M-bind(Mnd) z (λx.(M-return(Mnd) (g x))))))
    ∈ (cat-arrow(TypeCat) (M-map(Mnd) X) (M-map(Mnd) z)))

3
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:cat-ob(TypeCat)
    ((λz.(M-bind(Mnd) z (λx@0.(M-return(Mnd) (cat-id(TypeCat) X x@0)))))
    = (cat-id(TypeCat) (M-map(Mnd) X))
    ∈ (cat-arrow(TypeCat) (M-map(Mnd) X) (M-map(Mnd) X)))

---

Latex:

---

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


By

---

Latex:
(MemCD  THEN  Try  (QuickAuto))

---

Home Index