Nuprl Lemma : context-set-update-context4
∀X:?CubicalContext
(context-ok(X)
⇒ (∀[phi:Provisional''''(cttTerm(context-set(X)))]
∀X':?CubicalContext
((X' = update-context4{i:l}(X;phi) ∈ ?CubicalContext)
⇒ {allowed(phi)
⇒ type(allow(phi))=𝔽
⇒ (context-ok(X') ∧ (context-set(X') = context-set(X), term(allow(phi)) ∈ CubicalSet'''))})))
Proof
Definitions occuring in Statement :
update-context4: update-context4{i:l}(X;phi),
context-set: context-set(ctxt),
context-ok: context-ok(ctxt),
cubical-context: ?CubicalContext,
ctt-term-term: term(t),
ctt-term-type-is: type(t)=T,
ctt-term-meaning: cttTerm(X),
context-subset: Gamma, phi,
face-type: 𝔽,
cubical_set: CubicalSet,
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 :
all: ∀x:A. B[x],
implies: P ⇒ Q,
uall: ∀[x:A]. B[x],
guard: {T},
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-context4: update-context4{i:l}(X;phi),
context-ok: context-ok(ctxt),
bind-provision: bind-provision(x;t.f[t]),
restrict-cubical-context: restrict-cubical-context{i:l}(ctxt;trm),
allowed: allowed(x),
provision: provision(ok; v),
pi1: fst(t),
context-set: context-set(ctxt),
cubical-context: ?CubicalContext,
bind-provision: Error :bind-provision,
cubical_context: CubicalContext,
spreadn: spread3
Lemmas referenced :
ctt-term-type-is_wf,
context-set_wf,
allow_wf,
ctt-term-meaning_wf,
face-type_wf,
allowed_wf,
update-context4_wf,
provisional-type_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,
ctt-term-type-is-implies,
context-subset_wf,
istype-cubical-term
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
isect_memberFormation_alt,
cut,
independent_pairFormation,
hypothesis,
universeIsType,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
independent_isectElimination,
instantiate,
cumulativity,
equalityIstype,
because_Cache,
inhabitedIsType,
applyEquality,
lambdaEquality_alt,
imageElimination,
equalityTransitivity,
equalitySymmetry,
natural_numberEquality,
sqequalRule,
imageMemberEquality,
baseClosed,
universeEquality,
productElimination,
independent_functionElimination,
dependent_functionElimination,
Error :memTop,
productEquality,
dependent_set_memberEquality_alt,
productIsType,
applyLambdaEquality,
setElimination,
rename,
hyp_replacement
Latex:
\mforall{}X:?CubicalContext
(context-ok(X)
{}\mRightarrow{} (\mforall{}[phi:Provisional''''(cttTerm(context-set(X)))]
\mforall{}X':?CubicalContext
((X' = update-context4\{i:l\}(X;phi))
{}\mRightarrow{} \{allowed(phi)
{}\mRightarrow{} type(allow(phi))=\mBbbF{}
{}\mRightarrow{} (context-ok(X') \mwedge{} (context-set(X') = context-set(X), term(allow(phi))))\})))
Date html generated:
2020_05_20-PM-08_15_24
Last ObjectModification:
2020_05_18-AM-10_07_19
Theory : cubical!type!theory
Home
Index