---

Step * 4 1 2 of Lemma monad-from_wf

.....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)))
BY
{ (Intros THEN (FunExt THENA Auto) THEN Reduce 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)
3. A : Type@i'
4. B : Type@i'
5. g : A ⟶ B@i
6. x : M-map(Mnd) (M-map(Mnd) A)
⊢ (M-bind(Mnd) (M-bind(Mnd) x (λx.x)) (λx.(M-return(Mnd) (g x))))
= (M-bind(Mnd) (M-bind(Mnd) x (λx.(M-return(Mnd) (M-bind(Mnd) x (λx.(M-return(Mnd) (g x))))))) (λx.x))
∈ (M-map(Mnd) B)

---

Latex:

---

Latex:
.....set  predicate..... 
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{}  \mforall{}A,B:Type.  \mforall{}g:A  {}\mrightarrow{}  B.
        ((\mlambda{}x.(M-bind(Mnd)  ((\mlambda{}x,z.  (M-bind(Mnd)  z  (\mlambda{}x.x)))  A  x)  (\mlambda{}x.(M-return(Mnd)  (g  x)))))
        =  (\mlambda{}x.((\mlambda{}x,z.  (M-bind(Mnd)  z  (\mlambda{}x.x)))  B 
                      (M-bind(Mnd)  x  (\mlambda{}x.(M-return(Mnd)  (M-bind(Mnd)  x  (\mlambda{}x.(M-return(Mnd)  (g  x))))))))))


By

---

Latex:
(Intros  THEN  (FunExt  THENA  Auto)  THEN  Reduce  0)

---

Home Index