Nuprl Lemma : formal-cube-singleton-iso-interval-presheaf
∀x:ℕ. cat-isomorphic(FUN(op-cat(CubeCat);TypeCat');formal-cube({x});𝕀)
Proof
Definitions occuring in Statement :
formal-cube: formal-cube(I),
interval-presheaf: 𝕀,
cube-cat: CubeCat,
fset-singleton: {x},
nat: ℕ,
all: ∀x:A. B[x],
type-cat: TypeCat,
op-cat: op-cat(C),
functor-cat: FUN(C1;C2),
cat-isomorphic: cat-isomorphic(C;x;y)
Definitions unfolded in proof :
all: ∀x:A. B[x],
functor-cat: FUN(C1;C2),
cat-isomorphic: cat-isomorphic(C;x;y),
member: t ∈ T,
cat-isomorphism: cat-isomorphism(C;x;y;f),
exists: ∃x:A. B[x],
uall: ∀[x:A]. B[x],
cubical_set: CubicalSet,
ps_context: __⊢,
and: P ∧ Q,
cat-inverse: fg=1,
type-cat: TypeCat,
op-cat: op-cat(C),
cube-cat: CubeCat,
spreadn: spread4,
compose: f o g,
subtype_rel: A ⊆r B,
small_cubical_set: SmallCubicalSet,
cat-functor: Functor(C1;C2),
small_ps_context: small_ps_context{i:l}(C),
so_lambda: λ2x.t[x],
prop: ℙ,
so_apply: x[s],
uimplies: b supposing a,
fset: fset(T),
quotient: x,y:A//B[x; y],
cat-ob: cat-ob(C),
pi1: fst(t),
cat-arrow: cat-arrow(C),
pi2: snd(t),
names-hom: I ⟶ J,
implies: P ⇒ Q,
nh-id: 1,
nh-comp: g ⋅ f,
dma-lift-compose: dma-lift-compose(I;J;eqi;eqj;f;g),
cat-id: cat-id(C),
cat-comp: cat-comp(C),
trans-comp: t1 o t2,
mk-nat-trans: x |→ T[x],
formal-cube: formal-cube(I),
nat: ℕ,
uiff: uiff(P;Q),
names: names(I),
identity-trans: identity-trans(C;D;F),
DeMorgan-algebra: DeMorganAlgebra,
guard: {T},
sq_type: SQType(T)
Lemmas referenced :
istype-nat,
cat_arrow_triple_lemma,
formal-cube-singleton1,
formal-cube-singleton2,
formal-cube_wf,
fset-singleton_wf,
nat_wf,
cat_comp_tuple_lemma,
cat_id_tuple_lemma,
interval-presheaf_wf,
cat_ob_pair_lemma,
subtype_rel_sets,
cat-ob_wf,
op-cat_wf,
cube-cat_wf,
type-cat_wf,
cat-arrow_wf,
fset_wf,
names-hom_wf,
equal_wf,
cat-id_wf,
cat-comp_wf,
equal-wf-T-base,
nh-id_wf,
nh-comp_wf,
istype-universe,
subtype_rel_set,
subtype_rel_product,
subtype_rel_dep_function,
subtype_rel_self,
subtype_rel_universe1,
identity-trans_wf,
ob_pair_lemma,
member-fset-singleton,
int-deq_wf,
strong-subtype-deq-subtype,
strong-subtype-set3,
le_wf,
istype-int,
strong-subtype-self,
fset-member_wf,
names_wf,
nat-trans-equal,
lattice-point_wf,
dM_wf,
DeMorgan-algebra-structure_wf,
lattice-structure_wf,
lattice-axioms_wf,
bounded-lattice-structure-subtype,
DeMorgan-algebra-structure-subtype,
subtype_rel_transitivity,
bounded-lattice-structure_wf,
bounded-lattice-axioms_wf,
lattice-meet_wf,
lattice-join_wf,
DeMorgan-algebra-axioms_wf,
subtype_base_sq,
set_subtype_base,
int_subtype_base,
cat-inverse_wf,
functor-cat_wf,
formal-cube_wf1,
small_cubical_set_subtype,
nat-trans_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
cut,
introduction,
extract_by_obid,
hypothesis,
sqequalRule,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
Error :memTop,
dependent_pairFormation_alt,
hypothesisEquality,
isectElimination,
independent_pairFormation,
applyEquality,
instantiate,
cumulativity,
productEquality,
functionEquality,
universeEquality,
lambdaEquality_alt,
spreadEquality,
productIsType,
functionIsType,
universeIsType,
because_Cache,
inhabitedIsType,
baseClosed,
independent_isectElimination,
productElimination,
equalityIstype,
equalitySymmetry,
equalityTransitivity,
intEquality,
natural_numberEquality,
dependent_set_memberEquality_alt,
functionExtensionality,
rename,
isectEquality,
independent_functionElimination,
setElimination
Latex:
\mforall{}x:\mBbbN{}. cat-isomorphic(FUN(op-cat(CubeCat);TypeCat');formal-cube(\{x\});\mBbbI{})
Date html generated:
2020_05_20-PM-01_40_20
Last ObjectModification:
2020_04_20-PM-00_38_37
Theory : cubical!type!theory
Home
Index