Nuprl Lemma : face-presheaf_wf1
𝔽 ∈ SmallCubicalSet
Proof
Definitions occuring in Statement :
face-presheaf: 𝔽,
small_cubical_set: SmallCubicalSet,
member: t ∈ T
Definitions unfolded in proof :
face-presheaf: 𝔽,
small_cubical_set: SmallCubicalSet,
member: t ∈ T,
small_ps_context: small_ps_context{i:l}(C),
cat-functor: Functor(C1;C2),
type-cat: TypeCat,
cat-arrow: cat-arrow(C),
cube-cat: CubeCat,
op-cat: op-cat(C),
cat-ob: cat-ob(C),
spreadn: spread4,
pi1: fst(t),
pi2: snd(t),
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B,
cat-comp: cat-comp(C),
cat-id: cat-id(C),
and: P ∧ Q,
cand: A c∧ B,
all: ∀x:A. B[x]
Lemmas referenced :
lattice-point_wf,
face_lattice_wf,
fset_wf,
nat_wf,
fl-morph_wf,
names-hom_wf,
fl-morph-id,
fl-morph-comp,
nh-id_wf,
nh-comp_wf,
compose_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
dependent_set_memberEquality_alt,
dependent_pairEquality_alt,
lambdaEquality_alt,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
applyEquality,
because_Cache,
universeIsType,
inhabitedIsType,
functionIsType,
lambdaFormation_alt,
dependent_functionElimination,
independent_pairFormation,
productElimination,
productIsType,
equalityIstype,
baseClosed,
sqequalBase,
equalitySymmetry
Latex:
\mBbbF{} \mmember{} SmallCubicalSet
Date html generated:
2020_05_20-PM-01_44_36
Last ObjectModification:
2020_04_03-PM-07_49_45
Theory : cubical!type!theory
Home
Index