Nuprl Lemma : cubical_context_cumulativity
CubicalContext ⊆r cubical_context{i':l}
Proof
Definitions occuring in Statement :
cubical_context: CubicalContext,
subtype_rel: A ⊆r B
Definitions unfolded in proof :
subtype_rel: A ⊆r B,
member: t ∈ T,
cubical_context: CubicalContext,
uall: ∀[x:A]. B[x],
prop: ℙ
Lemmas referenced :
cubical_set_cumulativity-i-j,
ctt-term-meaning-cumulativity,
varname_wf,
l_member_wf,
ctt-term-meaning_wf,
cubical_context_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaEquality_alt,
sqequalHypSubstitution,
productElimination,
thin,
dependent_pairEquality_alt,
cut,
hypothesisEquality,
applyEquality,
instantiate,
introduction,
extract_by_obid,
hypothesis,
sqequalRule,
functionExtensionality,
isectElimination,
setEquality,
functionIsType,
setIsType,
universeIsType,
productIsType,
inhabitedIsType
Latex:
CubicalContext \msubseteq{}r cubical\_context\{i':l\}
Date html generated:
2020_05_20-PM-08_01_41
Last ObjectModification:
2020_05_04-AM-10_06_22
Theory : cubical!type!theory
Home
Index