---

Step * of Lemma M-associative

∀[Mnd:Monad]. ∀[T,S,U:Type]. ∀[m:M-map(Mnd) T]. ∀[f:T ⟶ (M-map(Mnd) S)]. ∀[g:S ⟶ (M-map(Mnd) U)].
  ((M-bind(Mnd) (M-bind(Mnd) m f) g) = (M-bind(Mnd) m (λx.(M-bind(Mnd) (f x) g))) ∈ (M-map(Mnd) U))
BY
{ ((Auto THEN Unfold `monad` 1) THEN DProds THEN RepUR ``M-map M-bind M-return`` 0) }

1
1. M : Type ⟶ Type
2. return : ⋂T:Type. (T ⟶ (M T))
3. bind : ⋂T,S:Type.  ((M T) ⟶ (T ⟶ (M S)) ⟶ (M S))
4. leftunit : ∀[T,S:Type]. ∀[x:T]. ∀[f:T ⟶ (M S)].  ((bind (return x) f) = (f x) ∈ (M S))
5. rightunit : ∀[T:Type]. ∀[m:M T].  ((bind m return) = m ∈ (M T))
6. M5 : ∀[T,S,U:Type]. ∀[m:M T]. ∀[f:T ⟶ (M S)]. ∀[g:S ⟶ (M U)].
          ((bind (bind m f) g) = (bind m (λx.(bind (f x) g))) ∈ (M U))
7. T : Type
8. S : Type
9. U : Type
10. m : M-map(<M, return, bind, leftunit, rightunit, M5>) T
11. f : T ⟶ (M-map(<M, return, bind, leftunit, rightunit, M5>) S)
12. g : S ⟶ (M-map(<M, return, bind, leftunit, rightunit, M5>) U)
⊢ (bind (bind m f) g) = (bind m (λx.(bind (f x) g))) ∈ (M U)

---

Latex:

---

Latex:
\mforall{}[Mnd:Monad].  \mforall{}[T,S,U:Type].  \mforall{}[m:M-map(Mnd)  T].  \mforall{}[f:T  {}\mrightarrow{}  (M-map(Mnd)  S)].  \mforall{}[g:S  {}\mrightarrow{}  (M-map(Mnd)  U)].
    ((M-bind(Mnd)  (M-bind(Mnd)  m  f)  g)  =  (M-bind(Mnd)  m  (\mlambda{}x.(M-bind(Mnd)  (f  x)  g))))


By

---

Latex:
((Auto  THEN  Unfold  `monad`  1)  THEN  DProds  THEN  RepUR  ``M-map  M-bind  M-return``  0)

---

Home Index