Nuprl Lemma : cubical_set_cumulativity-i-j
CubicalSet ⊆r cubical_set{[j | i]:l}
Proof
Definitions occuring in Statement :
cubical_set: CubicalSet,
subtype_rel: A ⊆r B
Definitions unfolded in proof :
subtype_rel: A ⊆r B,
member: t ∈ T,
cubical_set: CubicalSet,
ps_context: __⊢,
cat-functor: Functor(C1;C2),
type-cat: TypeCat,
cat-ob: cat-ob(C),
pi1: fst(t),
uall: ∀[x:A]. B[x],
cat-arrow: cat-arrow(C),
pi2: snd(t),
cat-comp: cat-comp(C),
cat-id: cat-id(C),
and: P ∧ Q,
all: ∀x:A. B[x]
Lemmas referenced :
cat-ob_wf,
op-cat_wf,
cube-cat_wf,
subtype_rel_self,
cat-arrow_wf,
type-cat_wf,
cat-id_wf,
cat-comp_wf,
cubical_set_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaEquality_alt,
sqequalHypSubstitution,
setElimination,
thin,
rename,
cut,
dependent_set_memberEquality_alt,
productElimination,
dependent_pairEquality_alt,
functionExtensionality,
applyEquality,
hypothesisEquality,
sqequalRule,
cumulativity,
universeIsType,
universeEquality,
hypothesis,
introduction,
extract_by_obid,
isectElimination,
instantiate,
functionEquality,
because_Cache,
functionIsType,
productIsType,
equalityIstype
Latex:
CubicalSet \msubseteq{}r cubical\_set\{[j | i]:l\}
Date html generated:
2020_05_20-PM-01_38_39
Last ObjectModification:
2020_04_03-PM-03_37_45
Theory : cubical!type!theory
Home
Index