### Nuprl Lemma : M-leftunit

`∀[Mnd:Monad]. ∀[T,S:Type]. ∀[x:T]. ∀[f:T ⟶ (M-map(Mnd) S)].`
`  ((M-bind(Mnd) (M-return(Mnd) x) f) = (f x) ∈ (M-map(Mnd) S))`

Proof

Definitions occuring in Statement :  M-bind: `M-bind(Mnd)` M-return: `M-return(Mnd)` M-map: `M-map(mnd)` monad: `Monad` uall: `∀[x:A]. B[x]` apply: `f a` 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-return: `M-return(Mnd)` 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 introduction cut sqequalHypSubstitution productElimination thin sqequalRule hypothesis functionEquality hypothesisEquality applyEquality lemma_by_obid isectElimination isect_memberEquality axiomEquality because_Cache universeEquality

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

Date html generated: 2016_05_15-PM-02_16_23
Last ObjectModification: 2015_12_27-AM-08_59_27