`∀[M:Type ⟶ Type]. ∀[return:⋂T:Type. (T ⟶ (M T))]. ∀[bind:⋂T,S:Type.  ((M T) ⟶ (T ⟶ (M S)) ⟶ (M S))].`
`  (mk_monad(M;return;bind) ∈ Monad) supposing `
`     ((∀[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))) and `
`     (∀[T:Type]. ∀[m:M T].  ((bind m return) = m ∈ (M T))) and `
`     (∀[T,S:Type]. ∀[x:T].  ∀f:T ⟶ (M S). ((bind (return x) f) = (f x) ∈ (M S))))`

Proof

Definitions occuring in Statement :  mk_monad: `mk_monad(M;return;bind)` monad: `Monad` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` member: `t ∈ T` apply: `f a` lambda: `λx.A[x]` isect: `⋂x:A. B[x]` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` uimplies: `b supposing a` member: `t ∈ T` all: `∀x:A. B[x]` subtype_rel: `A ⊆r B` implies: `P `` Q` prop: `ℙ` mk_monad: `mk_monad(M;return;bind)` monad: `Monad` squash: `↓T` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` so_lambda: `λ2x.t[x]` so_apply: `x[s]` exists: `∃x:A. B[x]`
Lemmas referenced :  equal_wf istype-universe squash_wf true_wf subtype_rel_self iff_weakening_equal trivial-equal isect_subtype_rel_trivial subtype_rel_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule sqequalHypSubstitution axiomEquality equalityTransitivity hypothesis equalitySymmetry isectIsType because_Cache universeIsType applyEquality hypothesisEquality extract_by_obid isectElimination thin lambdaFormation_alt lambdaEquality_alt functionIsType inhabitedIsType dependent_functionElimination equalityIstype independent_functionElimination instantiate universeEquality dependent_pairEquality_alt isect_memberEquality_alt imageElimination natural_numberEquality imageMemberEquality baseClosed independent_isectElimination productElimination functionEquality cumulativity isectEquality dependent_pairFormation_alt productIsType

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[return:\mcap{}T:Type.  (T  {}\mrightarrow{}  (M  T))].  \mforall{}[bind:\mcap{}T,S:Type.
((M  T)  {}\mrightarrow{}  (T  {}\mrightarrow{}  (M  S))  {}\mrightarrow{}  (M  S))].
((\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)))))  and
(\mforall{}[T:Type].  \mforall{}[m:M  T].    ((bind  m  return)  =  m))  and
(\mforall{}[T,S:Type].  \mforall{}[x:T].    \mforall{}f:T  {}\mrightarrow{}  (M  S).  ((bind  (return  x)  f)  =  (f  x))))

Date html generated: 2019_10_15-AM-10_59_27
Last ObjectModification: 2018_12_08-PM-04_47_35