Nuprl Lemma : bind-provision_wf_context
∀[x:?CubicalContext]. ∀[f:CubicalContext ⟶ ?CubicalContext]. (bind-provision(x;t.f[t]) ∈ ?CubicalContext)
Proof
Definitions occuring in Statement :
cubical-context: ?CubicalContext,
cubical_context: CubicalContext,
uall: ∀[x:A]. B[x],
so_apply: x[s],
member: t ∈ T,
function: x:A ⟶ B[x],
bind-provision: bind-provision(x;t.f[t])
Definitions unfolded in proof :
cubical-context: ?CubicalContext,
uall: ∀[x:A]. B[x],
member: t ∈ T,
so_lambda: λ2x.t[x],
so_apply: x[s]
Lemmas referenced :
bind-provision_wf,
cubical_context_wf,
provisional-type_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
thin,
instantiate,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
hypothesis,
hypothesisEquality,
sqequalRule,
lambdaEquality_alt,
applyEquality,
universeIsType,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
functionIsType,
inhabitedIsType,
isect_memberEquality_alt,
isectIsTypeImplies
Latex:
\mforall{}[x:?CubicalContext]. \mforall{}[f:CubicalContext {}\mrightarrow{} ?CubicalContext].
(bind-provision(x;t.f[t]) \mmember{} ?CubicalContext)
Date html generated:
2020_05_20-PM-08_06_59
Last ObjectModification:
2020_05_17-PM-10_34_13
Theory : cubical!type!theory
Home
Index