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 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))].
(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