---

Step * 4 1 of Lemma monad-from_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)
⊢ λ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)))} 
BY
{ MemTypeCD }

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)) ∈ A:Type ⟶ (M-map(Mnd) (M-map(Mnd) A)) ⟶ (M-map(Mnd) A)

2
.....set predicate..... 
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)
⊢ ∀A,B:Type. ∀g:A ⟶ B.
    ((λx.(M-bind(Mnd) ((λx,z. (M-bind(Mnd) z (λx.x))) A x) (λx.(M-return(Mnd) (g x)))))
    = (λx.((λx,z. (M-bind(Mnd) z (λx.x))) 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)))

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

---

Latex:

---

Latex:

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{}  \{trans:A:Type  {}\mrightarrow{}  (M-map(Mnd)  (M-map(Mnd)  A))  {}\mrightarrow{}  (M-map(Mnd)  A)| 
                                                            \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:
MemTypeCD

---

Home Index