Nuprl Lemma : update-context2-ok
∀X:?CubicalContext
(context-ok(X)
⇒ (∀[v:varname()]. ∀[t:Provisional''''(cttType(context-set(X)))].
∀X':?CubicalContext. ((X' = update-context2(X;v;t) ∈ ?CubicalContext) ⇒ {allowed(t) ⇒ context-ok(X')})))
Proof
Definitions occuring in Statement :
update-context2: update-context2(X;v;t),
context-set: context-set(ctxt),
context-ok: context-ok(ctxt),
cubical-context: ?CubicalContext,
ctt-type-meaning: cttType(X),
varname: varname(),
uall: ∀[x:A]. B[x],
guard: {T},
all: ∀x:A. B[x],
implies: P ⇒ Q,
equal: s = t ∈ T,
allowed: allowed(x),
provisional-type: Provisional(T)
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
implies: P ⇒ Q,
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
guard: {T},
and: P ∧ Q,
prop: ℙ
Lemmas referenced :
context-set-update-context2,
cubical-type_wf,
context-set_wf,
composition-structure_wf,
ctt-type-meaning_wf,
update-context2_wf,
varname_wf,
context-ok_wf,
cubical-context_wf
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
hypothesis,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
independent_functionElimination,
isect_memberFormation_alt,
isectElimination,
instantiate,
productEquality,
cumulativity,
independent_isectElimination,
productElimination,
universeIsType,
equalityIstype,
inhabitedIsType
Latex:
\mforall{}X:?CubicalContext
(context-ok(X)
{}\mRightarrow{} (\mforall{}[v:varname()]. \mforall{}[t:Provisional''''(cttType(context-set(X)))].
\mforall{}X':?CubicalContext. ((X' = update-context2(X;v;t)) {}\mRightarrow{} \{allowed(t) {}\mRightarrow{} context-ok(X')\})))
Date html generated:
2020_05_20-PM-08_13_20
Last ObjectModification:
2020_05_05-AM-10_02_50
Theory : cubical!type!theory
Home
Index