Nuprl Lemma : mk_monad_wf

[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 f) g) (bind x.(bind (f x) g))) ∈ (M U))) and 
     (∀[T:Type]. ∀[m:M T].  ((bind return) m ∈ (M T))) and 
     (∀[T,S:Type]. ∀[x:T].  ∀f:T ⟶ (M S). ((bind (return x) f) (f x) ∈ (M S))))


Definitions occuring in Statement :  mk_monad: mk_monad(M;return;bind) monad: Monad uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] member: t ∈ T apply: a lambda: λx.A[x] isect: x:A. B[x] function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T all: x:A. B[x] subtype_rel: A ⊆B implies:  Q prop: mk_monad: mk_monad(M;return;bind) monad: Monad squash: T true: True guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  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

\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))].
    (mk\_monad(M;return;bind)  \mmember{}  Monad)  supposing 
          ((\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

Theory : monads

Home Index