Nuprl Lemma : bind-provision-cubical-context-equations
(∀[x:CubicalContext]. ∀[f:CubicalContext ⟶ ?CubicalContext]. (bind-provision(OK(x);u.f u) = (f x) ∈ ?CubicalContext))
∧ (∀[m:?CubicalContext]. (bind-provision(m;u.OK(u)) = m ∈ ?CubicalContext))
∧ (∀[m:?CubicalContext]. ∀[f,g:CubicalContext ⟶ ?CubicalContext].
(bind-provision(bind-provision(m;u.f u);u.g u) = bind-provision(m;u.bind-provision(f u;u.g u)) ∈ ?CubicalContext))
Proof
Definitions occuring in Statement :
cubical-context: ?CubicalContext,
cubical_context: CubicalContext,
uall: ∀[x:A]. B[x],
and: P ∧ Q,
true: True,
apply: f a,
function: x:A ⟶ B[x],
equal: s = t ∈ T,
bind-provision: bind-provision(x;t.f[t]),
provision: provision(ok; v)
Definitions unfolded in proof :
provisional-monad: provisional-monad{i:l}(),
monad: Monad,
mk_monad: mk_monad(M;return;bind),
member: t ∈ T,
pi2: snd(t),
pi1: fst(t),
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B,
all: ∀x:A. B[x],
implies: P ⇒ Q,
prop: ℙ,
uimplies: b supposing a,
so_lambda: λ2x.t[x],
so_apply: x[s],
and: P ∧ Q,
cubical-context: ?CubicalContext
Lemmas referenced :
provisional-monad_wf,
pi1_wf_top,
provisional-type_wf,
istype-universe,
pi2_wf,
equal_wf,
bind-provision_wf,
provision_wf,
true_wf,
squash_wf,
cubical_context_wf
Rules used in proof :
cut,
instantiate,
introduction,
extract_by_obid,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
applyLambdaEquality,
productElimination,
thin,
sqequalRule,
hypothesisEquality,
hypothesis,
isectElimination,
functionEquality,
universeEquality,
independent_pairEquality,
Error :memTop,
isect_memberEquality_alt,
applyEquality,
lambdaEquality_alt,
equalityTransitivity,
equalitySymmetry,
isectIsType,
inhabitedIsType,
functionIsType,
universeIsType,
lambdaFormation_alt,
equalityIstype,
dependent_functionElimination,
independent_functionElimination,
because_Cache,
isectEquality,
cumulativity,
productEquality,
independent_pairFormation
Latex:
(\mforall{}[x:CubicalContext]. \mforall{}[f:CubicalContext {}\mrightarrow{} ?CubicalContext].
(bind-provision(OK(x);u.f u) = (f x)))
\mwedge{} (\mforall{}[m:?CubicalContext]. (bind-provision(m;u.OK(u)) = m))
\mwedge{} (\mforall{}[m:?CubicalContext]. \mforall{}[f,g:CubicalContext {}\mrightarrow{} ?CubicalContext].
(bind-provision(bind-provision(m;u.f u);u.g u)
= bind-provision(m;u.bind-provision(f u;u.g u))))
Date html generated:
2020_05_20-PM-08_04_41
Last ObjectModification:
2020_05_17-PM-10_28_49
Theory : cubical!type!theory
Home
Index