Nuprl Lemma : context-set-update-context2
∀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') ∧ (context-set(X') = context-set(X).type(allow(t)) ∈ CubicalSet'''))})))
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-type: type(T),
ctt-type-meaning: cttType(X),
cube-context-adjoin: X.A,
cubical_set: CubicalSet,
varname: varname(),
uall: ∀[x:A]. B[x],
guard: {T},
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
equal: s = t ∈ T,
allow: allow(x),
allowed: allowed(x),
provisional-type: Provisional(T)
Definitions unfolded in proof :
guard: {T},
all: ∀x:A. B[x],
implies: P ⇒ Q,
uall: ∀[x:A]. B[x],
and: P ∧ Q,
cand: A c∧ B,
member: t ∈ T,
uimplies: b supposing a,
prop: ℙ,
squash: ↓T,
true: True,
subtype_rel: A ⊆r B,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
update-context2: update-context2(X;v;t),
context-ok: context-ok(ctxt),
bind-provision: bind-provision(x;t.f[t]),
update-cubical-context2: ctxt; v:fst(T),
cubical-context: ?CubicalContext,
context-set: context-set(ctxt),
bind-provision: Error :bind-provision,
cubical_context: CubicalContext,
pi1: fst(t),
ctt-type-meaning: cttType(X),
ctt-type-type: type(T),
update-context-lvl: update-context-lvl(ctxt;lvl;T;v),
spreadn: spread3,
pi2: snd(t)
Lemmas referenced :
allowed_wf,
ctt-type-meaning_wf,
context-set_wf,
update-context2_wf,
provisional-type_wf,
varname_wf,
context-ok_wf,
cubical-context_wf,
squash_wf,
true_wf,
subtype_rel_self,
iff_weakening_equal,
allowed_provision_lemma,
implies-usquash2,
cubical_context_wf,
usquash_wf,
allow_provision_lemma,
cube-context-adjoin_wf-level-type
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lambdaFormation_alt,
isect_memberFormation_alt,
cut,
independent_pairFormation,
hypothesis,
universeIsType,
thin,
instantiate,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
hypothesisEquality,
independent_isectElimination,
equalityIstype,
inhabitedIsType,
applyEquality,
lambdaEquality_alt,
imageElimination,
equalityTransitivity,
equalitySymmetry,
natural_numberEquality,
imageMemberEquality,
baseClosed,
universeEquality,
productElimination,
independent_functionElimination,
dependent_functionElimination,
Error :memTop,
productEquality,
dependent_set_memberEquality_alt,
productIsType,
applyLambdaEquality,
setElimination,
rename,
because_Cache
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') \mwedge{} (context-set(X') = context-set(X).type(allow(t))))\})))
Date html generated:
2020_05_20-PM-08_13_00
Last ObjectModification:
2020_05_18-AM-10_07_35
Theory : cubical!type!theory
Home
Index