---

Step * 4 1 3 of Lemma monad-from_wf

.....wf..... 
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. trans : A:Type ⟶ (M-map(Mnd) (M-map(Mnd) A)) ⟶ (M-map(Mnd) A)
⊢ istype(∀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))))
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
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.  trans  :  A:Type  {}\mrightarrow{}  (M-map(Mnd)  (M-map(Mnd)  A))  {}\mrightarrow{}  (M-map(Mnd)  A)
\mvdash{}  istype(\mforall{}A,B:Type.  \mforall{}g:A  {}\mrightarrow{}  B.
                      ((\mlambda{}x.(M-bind(Mnd)  (trans  A  x)  (\mlambda{}x.(M-return(Mnd)  (g  x)))))
                      =  (\mlambda{}x.(trans  B 
                                    (M-bind(Mnd)  x 
                                      (\mlambda{}x.(M-return(Mnd)  (M-bind(Mnd)  x  (\mlambda{}x.(M-return(Mnd)  (g  x)))))))))))


By

---

Latex:
Auto

---

Home Index