Nuprl Lemma : cubical_set_cumulativity-i-j

CubicalSet ⊆cubical_set{[j i]:l}


Proof




Definitions occuring in Statement :  cubical_set: CubicalSet subtype_rel: A ⊆B
Definitions unfolded in proof :  subtype_rel: A ⊆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