---

Step * of Lemma face-name-image

∀X:CubicalSet. ∀I:Cname List. ∀K,f:Top. ∀face:I-face(X;I).
  (face-name(face-image(X;I;K;f;face)) ~ (λp.<f (fst(p)), snd(p)>) face-name(face))
BY
{ (Intros THEN RepeatFor 2 (D -1) THEN RepUR ``face-name face-image`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}X:CubicalSet.  \mforall{}I:Cname  List.  \mforall{}K,f:Top.  \mforall{}face:I-face(X;I).
    (face-name(face-image(X;I;K;f;face))  \msim{}  (\mlambda{}p.<f  (fst(p)),  snd(p)>)  face-name(face))


By

---

Latex:
(Intros  THEN  RepeatFor  2  (D  -1)  THEN  RepUR  ``face-name  face-image``  0  THEN  Auto)

---

Home Index