### Nuprl 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))`

Proof

Definitions occuring in Statement :  M-bind: `M-bind(Mnd)` M-map: `M-map(mnd)` monad: `Monad` uall: `∀[x:A]. B[x]` apply: `f a` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` monad: `Monad` M-bind: `M-bind(Mnd)` M-map: `M-map(mnd)` pi1: `fst(t)` pi2: `snd(t)`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalHypSubstitution productElimination thin sqequalRule hypothesis functionIsType universeIsType hypothesisEquality applyEquality extract_by_obid isectElimination isect_memberEquality axiomEquality functionEquality because_Cache inhabitedIsType universeEquality

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))))

Date html generated: 2019_10_15-AM-10_59_21
Last ObjectModification: 2018_09_27-AM-11_06_11