---

Step * of Lemma unit-cube-map_wf

∀[I,J:Cname List]. ∀[f:name-morph(I;J)].  (unit-cube-map(f) ∈ unit-cube(J) ⟶ unit-cube(I))
BY
{ (Intros
   THEN Unfold `unit-cube-map` 0
   THEN (MemTypeCD THENW Auto)
   THEN All (RepUR ``cat-ob cat-arrow cat-comp type-cat name-cat unit-cube``)
   THEN All (RepUR ``functor-ob functor-arrow compose``)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I,J:Cname  List].  \mforall{}[f:name-morph(I;J)].    (unit-cube-map(f)  \mmember{}  unit-cube(J)  {}\mrightarrow{}  unit-cube(I))


By

---

Latex:
(Intros
  THEN  Unfold  `unit-cube-map`  0
  THEN  (MemTypeCD  THENW  Auto)
  THEN  All  (RepUR  ``cat-ob  cat-arrow  cat-comp  type-cat  name-cat  unit-cube``)
  THEN  All  (RepUR  ``functor-ob  functor-arrow  compose``)
  THEN  Auto)

---

Home Index