---

Step * 6 1 1 of Lemma monad-from_wf

.....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. x : M-map(Mnd) X
5. ∀[f:X ⟶ (M-map(Mnd) (M-map(Mnd) X))]. ∀[g:(M-map(Mnd) X) ⟶ (M-map(Mnd) X)].
     ((M-bind(Mnd) (M-bind(Mnd) x f) g) = (M-bind(Mnd) x (λx.(M-bind(Mnd) (f x) g))) ∈ (M-map(Mnd) X))
6. (M-bind(Mnd) x M-return(Mnd)) = x ∈ (M-map(Mnd) X)
⊢ (M-bind(Mnd) x (λx.(M-bind(Mnd) (M-return(Mnd) (M-return(Mnd) x)) (λx.x))))
= (M-bind(Mnd) x M-return(Mnd))
∈ (M-map(Mnd) X)
BY
{ ((Assert M-bind(Mnd) ∈ (M-map(Mnd) X) ⟶ (X ⟶ (M-map(Mnd) X)) ⟶ (M-map(Mnd) X) BY
          Auto)
   THEN EqCDA
   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. X : Type
4. x : M-map(Mnd) X
5. ∀[f:X ⟶ (M-map(Mnd) (M-map(Mnd) X))]. ∀[g:(M-map(Mnd) X) ⟶ (M-map(Mnd) X)].
     ((M-bind(Mnd) (M-bind(Mnd) x f) g) = (M-bind(Mnd) x (λx.(M-bind(Mnd) (f x) g))) ∈ (M-map(Mnd) X))
6. (M-bind(Mnd) x M-return(Mnd)) = x ∈ (M-map(Mnd) X)
7. M-bind(Mnd) ∈ (M-map(Mnd) X) ⟶ (X ⟶ (M-map(Mnd) X)) ⟶ (M-map(Mnd) X)
8. x1 : X
⊢ (M-bind(Mnd) (M-return(Mnd) (M-return(Mnd) x1)) (λx.x)) = (M-return(Mnd) x1) ∈ (M-map(Mnd) X)

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
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.  x  :  M-map(Mnd)  X
5.  \mforall{}[f:X  {}\mrightarrow{}  (M-map(Mnd)  (M-map(Mnd)  X))].  \mforall{}[g:(M-map(Mnd)  X)  {}\mrightarrow{}  (M-map(Mnd)  X)].
          ((M-bind(Mnd)  (M-bind(Mnd)  x  f)  g)  =  (M-bind(Mnd)  x  (\mlambda{}x.(M-bind(Mnd)  (f  x)  g))))
6.  (M-bind(Mnd)  x  M-return(Mnd))  =  x
\mvdash{}  (M-bind(Mnd)  x  (\mlambda{}x.(M-bind(Mnd)  (M-return(Mnd)  (M-return(Mnd)  x))  (\mlambda{}x.x))))
=  (M-bind(Mnd)  x  M-return(Mnd))


By

---

Latex:
((Assert  M-bind(Mnd)  \mmember{}  (M-map(Mnd)  X)  {}\mrightarrow{}  (X  {}\mrightarrow{}  (M-map(Mnd)  X))  {}\mrightarrow{}  (M-map(Mnd)  X)  BY
                Auto)
  THEN  EqCDA
  THEN  (FunExt  THENA  Auto)
  THEN  Reduce  0)

---

Home Index