Nuprl Lemma : update-cubical-context2_wf
∀[ctxt:CubicalContext]. ∀[v:varname()]. ∀[T:Provisional''''(ctt-type-meaning1{i:l}(fst(ctxt)))].
(ctxt; v:fst(T) ∈ ?CubicalContext)
Proof
Definitions occuring in Statement :
update-cubical-context2: ctxt; v:fst(T),
cubical-context: ?CubicalContext,
cubical_context: CubicalContext,
ctt-type-meaning1: ctt-type-meaning1{i:l}(X),
varname: varname(),
uall: ∀[x:A]. B[x],
pi1: fst(t),
member: t ∈ T,
provisional-type: Provisional(T)
Definitions unfolded in proof :
cubical-context: ?CubicalContext,
uall: ∀[x:A]. B[x],
member: t ∈ T,
update-cubical-context2: ctxt; v:fst(T),
cubical_context: CubicalContext,
prop: ℙ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
pi1: fst(t),
uimplies: b supposing a,
ctt-type-meaning1: ctt-type-meaning1{i:l}(X),
spreadn: spread3
Lemmas referenced :
ctt-type-meaning1_wf,
pi1_wf_top,
cubical_set_wf,
cubical_context_wf,
update-context-lvl_wf,
l_member_wf,
varname_wf,
ctt-term-meaning_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
cut,
thin,
instantiate,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
cumulativity,
hypothesis,
productElimination,
independent_pairEquality,
hypothesisEquality,
Error :memTop,
isect_memberEquality_alt,
inhabitedIsType,
lambdaFormation_alt,
sqequalRule,
equalityIstype,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination,
independent_functionElimination,
independent_isectElimination,
dependent_pairEquality_alt,
functionIsType,
setIsType,
universeIsType,
productIsType
Latex:
\mforall{}[ctxt:CubicalContext]. \mforall{}[v:varname()]. \mforall{}[T:Provisional''''(ctt-type-meaning1\{i:l\}(fst(ctxt)))].
(ctxt; v:fst(T) \mmember{} ?CubicalContext)
Date html generated:
2020_05_20-PM-08_10_39
Last ObjectModification:
2020_05_05-AM-09_45_05
Theory : cubical!type!theory
Home
Index