---

Step * of 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)))
BY
{ ((UnivCD THENA Auto)
   THEN RepeatFor 2 (D -2)
   THEN RepeatFor 2 (D -1)
   THEN (RWO "cubical-nerve-I-cube" (-1) THENA Auto)
   THEN RepUR ``face-compatible cube-set-restriction cubical-nerve I-cube functor-ob`` 0
   THEN Auto) }

---

Latex:

---

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)))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepeatFor  2  (D  -2)
  THEN  RepeatFor  2  (D  -1)
  THEN  (RWO  "cubical-nerve-I-cube"  (-1)  THENA  Auto)
  THEN  RepUR  ``face-compatible  cube-set-restriction  cubical-nerve  I-cube  functor-ob``  0
  THEN  Auto)

---

Home Index