Step
*
of Lemma
A-face-name-image
∀X:CubicalSet. ∀A:{X ⊢ _}. ∀I:Cname List. ∀alpha:X(I). ∀K,f:Top. ∀face:A-face(X;A;I;alpha).
(A-face-name(A-face-image(X;A;I;K;f;alpha;face)) ~ (λp.<f (fst(p)), snd(p)>) A-face-name(face))
BY
{ (Intros THEN RepeatFor 2 (D -1) THEN RepUR ``A-face-name A-face-image`` 0 THEN Auto) }
Latex:
Latex:
\mforall{}X:CubicalSet. \mforall{}A:\{X \mvdash{} \_\}. \mforall{}I:Cname List. \mforall{}alpha:X(I). \mforall{}K,f:Top. \mforall{}face:A-face(X;A;I;alpha).
(A-face-name(A-face-image(X;A;I;K;f;alpha;face)) \msim{} (\mlambda{}p.<f (fst(p)), snd(p)>) A-face-name(face))
By
Latex:
(Intros THEN RepeatFor 2 (D -1) THEN RepUR ``A-face-name A-face-image`` 0 THEN Auto)
Home
Index