Nuprl Lemma : restrict-cubical-context_wf
∀[ctxt:CubicalContext]. ∀[trm:Provisional''''(cttTerm(fst(ctxt)))].
(restrict-cubical-context{i:l}(ctxt;trm) ∈ ?CubicalContext)
Proof
Definitions occuring in Statement :
restrict-cubical-context: restrict-cubical-context{i:l}(ctxt;trm),
cubical-context: ?CubicalContext,
cubical_context: CubicalContext,
ctt-term-meaning: cttTerm(X),
uall: ∀[x:A]. B[x],
pi1: fst(t),
member: t ∈ T,
provisional-type: Provisional(T)
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
cubical_context: CubicalContext,
pi1: fst(t),
restrict-cubical-context: restrict-cubical-context{i:l}(ctxt;trm),
cubical-context: ?CubicalContext,
spreadn: spread3,
and: P ∧ Q,
prop: ℙ,
uimplies: b supposing a,
all: ∀x:A. B[x],
implies: P ⇒ Q,
subtype_rel: A ⊆r B
Lemmas referenced :
ctt-term-meaning_wf,
ctt-term-type-is_wf,
face-type_wf,
cubical_context_wf,
ctt-term-type-is-implies,
context-subset_wf,
ctt-term-meaning-subtype,
context-subset-is-subset,
varname_wf,
l_member_wf,
pi1_wf_top,
cubical_set_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
cut,
sqequalHypSubstitution,
productElimination,
thin,
sqequalRule,
productEquality,
instantiate,
introduction,
extract_by_obid,
isectElimination,
cumulativity,
hypothesisEquality,
hypothesis,
independent_isectElimination,
isect_memberEquality_alt,
inhabitedIsType,
lambdaFormation_alt,
dependent_pairEquality_alt,
functionExtensionality,
applyEquality,
setEquality,
functionIsType,
setIsType,
universeIsType,
productIsType,
equalityIstype,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination,
independent_functionElimination,
independent_pairEquality,
Error :memTop
Latex:
\mforall{}[ctxt:CubicalContext]. \mforall{}[trm:Provisional''''(cttTerm(fst(ctxt)))].
(restrict-cubical-context\{i:l\}(ctxt;trm) \mmember{} ?CubicalContext)
Date html generated:
2020_05_20-PM-08_11_19
Last ObjectModification:
2020_05_11-AM-10_29_56
Theory : cubical!type!theory
Home
Index