---

Step * 3 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)
3. A : Type
4. B : Type
5. g : A ⟶ B
⊢ ((λz.(M-bind(Mnd) z (λx.(M-return(Mnd) (g x))))) o ((λx.M-return(Mnd)) A))
= (((λx.M-return(Mnd)) B) o g)
∈ (A ⟶ (M-map(Mnd) B))
BY
{ ((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
4. B : Type
5. g : A ⟶ B
6. x : A
⊢ (M-bind(Mnd) (M-return(Mnd) x) (λx.(M-return(Mnd) (g x)))) = (M-return(Mnd) (g x)) ∈ (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)
3.  A  :  Type
4.  B  :  Type
5.  g  :  A  {}\mrightarrow{}  B
\mvdash{}  ((\mlambda{}z.(M-bind(Mnd)  z  (\mlambda{}x.(M-return(Mnd)  (g  x)))))  o  ((\mlambda{}x.M-return(Mnd))  A))
=  (((\mlambda{}x.M-return(Mnd))  B)  o  g)


By

---

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

---

Home Index