---

Step * 1 2 2 of Lemma mk_monad_wf

.....subterm..... T:t
2:n
1. M : Type ⟶ Type
2. return : ⋂T:Type. (T ⟶ (M T))
3. bind : ⋂T,S:Type.  ((M T) ⟶ (T ⟶ (M S)) ⟶ (M S))
4. ∀[T,S:Type]. ∀[x:T].  ∀f:T ⟶ (M S). ((bind (return x) f) = (f x) ∈ (M S))
5. ∀[T:Type]. ∀[m:M T].  ((bind m return) = m ∈ (M T))
6. ∀[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))
⊢ <bind, Ax, Ax, Ax> ∈ bind:⋂T,S:Type.  ((M T) ⟶ (T ⟶ (M S)) ⟶ (M S))
  × leftunit:∀[T,S:Type]. ∀[x:T]. ∀[f:T ⟶ (M S)].  ((bind (return x) f) = (f x) ∈ (M S))
  × rightunit:∀[T:Type]. ∀[m:M T].  ((bind m return) = m ∈ (M T))
  × (∀[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)))
BY
{ MemCD }

1
.....subterm..... T:t
1:n
1. M : Type ⟶ Type
2. return : ⋂T:Type. (T ⟶ (M T))
3. bind : ⋂T,S:Type.  ((M T) ⟶ (T ⟶ (M S)) ⟶ (M S))
4. ∀[T,S:Type]. ∀[x:T].  ∀f:T ⟶ (M S). ((bind (return x) f) = (f x) ∈ (M S))
5. ∀[T:Type]. ∀[m:M T].  ((bind m return) = m ∈ (M T))
6. ∀[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))
⊢ bind ∈ ⋂T,S:Type.  ((M T) ⟶ (T ⟶ (M S)) ⟶ (M S))

2
.....subterm..... T:t
2:n
1. M : Type ⟶ Type
2. return : ⋂T:Type. (T ⟶ (M T))
3. bind : ⋂T,S:Type.  ((M T) ⟶ (T ⟶ (M S)) ⟶ (M S))
4. ∀[T,S:Type]. ∀[x:T].  ∀f:T ⟶ (M S). ((bind (return x) f) = (f x) ∈ (M S))
5. ∀[T:Type]. ∀[m:M T].  ((bind m return) = m ∈ (M T))
6. ∀[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))
⊢ <Ax, Ax, Ax> ∈ leftunit:∀[T,S:Type]. ∀[x:T]. ∀[f:T ⟶ (M S)].  ((bind (return x) f) = (f x) ∈ (M S))
  × rightunit:∀[T:Type]. ∀[m:M T].  ((bind m return) = m ∈ (M T))
  × (∀[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)))

3
.....eq aux..... 
1. M : Type ⟶ Type
2. return : ⋂T:Type. (T ⟶ (M T))
3. bind : ⋂T,S:Type.  ((M T) ⟶ (T ⟶ (M S)) ⟶ (M S))
4. ∀[T,S:Type]. ∀[x:T].  ∀f:T ⟶ (M S). ((bind (return x) f) = (f x) ∈ (M S))
5. ∀[T:Type]. ∀[m:M T].  ((bind m return) = m ∈ (M T))
6. ∀[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. b1 : ⋂T,S:Type.  ((M T) ⟶ (T ⟶ (M S)) ⟶ (M S))
⊢ istype(leftunit:∀[T,S:Type]. ∀[x:T]. ∀[f:T ⟶ (M S)].  ((b1 (return x) f) = (f x) ∈ (M S))
× rightunit:∀[T:Type]. ∀[m:M T].  ((b1 m return) = m ∈ (M T))
× (∀[T,S,U:Type]. ∀[m:M T]. ∀[f:T ⟶ (M S)]. ∀[g:S ⟶ (M U)].  ((b1 (b1 m f) g) = (b1 m (λx.(b1 (f x) g))) ∈ (M U))))

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  M  :  Type  {}\mrightarrow{}  Type
2.  return  :  \mcap{}T:Type.  (T  {}\mrightarrow{}  (M  T))
3.  bind  :  \mcap{}T,S:Type.    ((M  T)  {}\mrightarrow{}  (T  {}\mrightarrow{}  (M  S))  {}\mrightarrow{}  (M  S))
4.  \mforall{}[T,S:Type].  \mforall{}[x:T].    \mforall{}f:T  {}\mrightarrow{}  (M  S).  ((bind  (return  x)  f)  =  (f  x))
5.  \mforall{}[T:Type].  \mforall{}[m:M  T].    ((bind  m  return)  =  m)
6.  \mforall{}[T,S,U:Type].  \mforall{}[m:M  T].  \mforall{}[f:T  {}\mrightarrow{}  (M  S)].  \mforall{}[g:S  {}\mrightarrow{}  (M  U)].
          ((bind  (bind  m  f)  g)  =  (bind  m  (\mlambda{}x.(bind  (f  x)  g))))
\mvdash{}  <bind,  Ax,  Ax,  Ax>  \mmember{}  bind:\mcap{}T,S:Type.    ((M  T)  {}\mrightarrow{}  (T  {}\mrightarrow{}  (M  S))  {}\mrightarrow{}  (M  S))
    \mtimes{}  leftunit:\mforall{}[T,S:Type].  \mforall{}[x:T].  \mforall{}[f:T  {}\mrightarrow{}  (M  S)].    ((bind  (return  x)  f)  =  (f  x))
    \mtimes{}  rightunit:\mforall{}[T:Type].  \mforall{}[m:M  T].    ((bind  m  return)  =  m)
    \mtimes{}  (\mforall{}[T,S,U:Type].  \mforall{}[m:M  T].  \mforall{}[f:T  {}\mrightarrow{}  (M  S)].  \mforall{}[g:S  {}\mrightarrow{}  (M  U)].
              ((bind  (bind  m  f)  g)  =  (bind  m  (\mlambda{}x.(bind  (f  x)  g)))))


By

---

Latex:
MemCD

---

Home Index