---

Step * 2 2 1 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. X : Type
4. Y : Type
5. z : Type
6. f : X ⟶ Y
7. g : Y ⟶ z
8. x : M-map(Mnd) X
⊢ (M-bind(Mnd) x (λx@0.(M-return(Mnd) (g (f x@0)))))
= (M-bind(Mnd) x (λx.(M-bind(Mnd) ((λx.(M-return(Mnd) (f x))) x) (λx.(M-return(Mnd) (g x))))))
∈ (M-map(Mnd) z)
BY
{ ((Assert M-bind(Mnd) ∈ (M-map(Mnd) X) ⟶ (X ⟶ (M-map(Mnd) z)) ⟶ (M-map(Mnd) z) BY Auto) THEN EqCD) }

1
.....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)
3. X : Type
4. Y : Type
5. z : Type
6. f : X ⟶ Y
7. g : Y ⟶ z
8. x : M-map(Mnd) X
9. M-bind(Mnd) ∈ (M-map(Mnd) X) ⟶ (X ⟶ (M-map(Mnd) z)) ⟶ (M-map(Mnd) z)
⊢ (M-bind(Mnd) x) = (M-bind(Mnd) x) ∈ ((X ⟶ (M-map(Mnd) z)) ⟶ (M-map(Mnd) z))

2
.....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 : Type
4. Y : Type
5. z : Type
6. f : X ⟶ Y
7. g : Y ⟶ z
8. x : M-map(Mnd) X
9. M-bind(Mnd) ∈ (M-map(Mnd) X) ⟶ (X ⟶ (M-map(Mnd) z)) ⟶ (M-map(Mnd) z)
⊢ (λx@0.(M-return(Mnd) (g (f x@0))))
= (λx.(M-bind(Mnd) ((λx.(M-return(Mnd) (f x))) x) (λx.(M-return(Mnd) (g x)))))
∈ (X ⟶ (M-map(Mnd) z))

---

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.  X  :  Type
4.  Y  :  Type
5.  z  :  Type
6.  f  :  X  {}\mrightarrow{}  Y
7.  g  :  Y  {}\mrightarrow{}  z
8.  x  :  M-map(Mnd)  X
\mvdash{}  (M-bind(Mnd)  x  (\mlambda{}x@0.(M-return(Mnd)  (g  (f  x@0)))))
=  (M-bind(Mnd)  x  (\mlambda{}x.(M-bind(Mnd)  ((\mlambda{}x.(M-return(Mnd)  (f  x)))  x)  (\mlambda{}x.(M-return(Mnd)  (g  x))))))


By

---

Latex:
((Assert  M-bind(Mnd)  \mmember{}  (M-map(Mnd)  X)  {}\mrightarrow{}  (X  {}\mrightarrow{}  (M-map(Mnd)  z))  {}\mrightarrow{}  (M-map(Mnd)  z)  BY  Auto)  THEN  EqCD)

---

Home Index