---

Step * of Lemma face-image_wf

∀[X:CubicalSet]. ∀[I,K:Cname List]. ∀[f:name-morph(I;K)]. ∀[face:I-face(X;I)].
  face-image(X;I;K;f;face) ∈ I-face(X;K) supposing ↑isname(f (fst(face)))
BY
{ (Intros
   THEN Unhide
   THEN Unfold `face-image` 0
   THEN DVar `face'
   THEN DVar `f1'
   THEN Reduce 0
   THEN Unfold `I-face` 0
   THEN Reduce (-1)) }

1
1. X : CubicalSet
2. I : Cname List
3. K : Cname List
4. f : name-morph(I;K)
5. x : nameset(I)
6. f2 : ℕ2
7. f3 : X(I-[x])
8. ↑isname(f x)
⊢ <f x, f2, f(f3)> ∈ x:nameset(K) × ℕ2 × X(K-[x])

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[I,K:Cname  List].  \mforall{}[f:name-morph(I;K)].  \mforall{}[face:I-face(X;I)].
    face-image(X;I;K;f;face)  \mmember{}  I-face(X;K)  supposing  \muparrow{}isname(f  (fst(face)))


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  Unfold  `face-image`  0
  THEN  DVar  `face'
  THEN  DVar  `f1'
  THEN  Reduce  0
  THEN  Unfold  `I-face`  0
  THEN  Reduce  (-1))

---

Home Index