Nuprl Lemma : face-compatible-cubical-nerve1
∀[C:SmallCategory]. ∀[I:Cname List].
∀f1,f2:I-face(cubical-nerve(C);I).
(face-compatible(cubical-nerve(C);I;f1;f2) ~ (¬((fst(f1)) = (fst(f2)) ∈ Cname))
⇒ (functor-comp(poset-functor(I-[fst(f1)];I-[fst(f1); fst(f2)];(fst(f2):=fst(snd(f2))));snd(snd(f1)))
= functor-comp(poset-functor(I-[fst(f2)];I-[fst(f1); fst(f2)];(fst(f1):=fst(snd(f1))));snd(snd(f2)))
∈ Functor(poset-cat(I-[fst(f1); fst(f2)]);C)))
Proof
Definitions occuring in Statement :
cubical-nerve: cubical-nerve(X),
poset-functor: poset-functor(J;K;f),
poset-cat: poset-cat(J),
face-compatible: face-compatible(X;I;f1;f2),
I-face: I-face(X;I),
face-map: (x:=i),
cname_deq: CnameDeq,
coordinate_name: Cname,
functor-comp: functor-comp(F;G),
cat-functor: Functor(C1;C2),
small-category: SmallCategory,
list-diff: as-bs,
cons: [a / b],
nil: [],
list: T List,
uall: ∀[x:A]. B[x],
pi1: fst(t),
pi2: snd(t),
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
sqequal: s ~ t,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
all: ∀x:A. B[x],
I-face: I-face(X;I),
top: Top,
cubical-nerve: cubical-nerve(X),
face-compatible: face-compatible(X;I;f1;f2),
spreadn: spread3,
pi1: fst(t),
pi2: snd(t),
cube-set-restriction: f(s),
I-cube: X(I),
functor-ob: functor-ob(F)
Lemmas referenced :
cubical-nerve-I-cube,
I-face_wf,
cubical-nerve_wf,
list_wf,
coordinate_name_wf,
small-category_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
lambdaFormation,
sqequalHypSubstitution,
productElimination,
thin,
lemma_by_obid,
isectElimination,
isect_memberEquality,
voidElimination,
voidEquality,
hypothesis,
sqequalRule,
hypothesisEquality,
lambdaEquality,
dependent_functionElimination,
sqequalAxiom,
because_Cache
Latex:
\mforall{}[C:SmallCategory]. \mforall{}[I:Cname List].
\mforall{}f1,f2:I-face(cubical-nerve(C);I).
(face-compatible(cubical-nerve(C);I;f1;f2) \msim{} (\mneg{}((fst(f1)) = (fst(f2))))
{}\mRightarrow{} (functor-comp(poset-functor(I-[fst(f1)];I-[fst(f1); fst(f2)];(fst(f2):=fst(snd(f2))));
snd(snd(f1)))
= functor-comp(poset-functor(I-[fst(f2)];I-[fst(f1); fst(f2)];(fst(f1):=fst(snd(f1))));
snd(snd(f2)))))
Date html generated:
2016_06_16-PM-07_02_08
Last ObjectModification:
2015_12_28-PM-04_18_30
Theory : cubical!sets
Home
Index