---

Step * of Lemma csm-ap_wf

∀[X,Y:CubicalSet]. ∀[s:X ⟶ Y]. ∀[I:Cname List]. ∀[x:X(I)].  ((s)x ∈ Y(I))
BY
{ (Auto
   THEN Unfold `csm-ap` 0
   THEN (RepeatFor 2 (D 1) THEN RepeatFor 2 (D 4))
   THEN All Reduce
   THEN All (RepUR ``I-cube functor-ob cube-set-map``)
   THEN D -3
   THEN RepUR ``cat-ob name-cat cat-arrow functor-ob type-cat`` -4
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X,Y:CubicalSet].  \mforall{}[s:X  {}\mrightarrow{}  Y].  \mforall{}[I:Cname  List].  \mforall{}[x:X(I)].    ((s)x  \mmember{}  Y(I))


By

---

Latex:
(Auto
  THEN  Unfold  `csm-ap`  0
  THEN  (RepeatFor  2  (D  1)  THEN  RepeatFor  2  (D  4))
  THEN  All  Reduce
  THEN  All  (RepUR  ``I-cube  functor-ob  cube-set-map``)
  THEN  D  -3
  THEN  RepUR  ``cat-ob  name-cat  cat-arrow  functor-ob  type-cat``  -4
  THEN  Auto)

---

Home Index