---

Step * of Lemma cubical-set-is-functor

CubicalSet ≡ Functor(NameCat;TypeCat)
BY
{ ((RepeatFor 2 (D 0) THENA Auto)
   THEN RepeatFor 2 (D 1)
   THEN Reduce (-1)
   THEN D -1
   THEN MemTypeCD
   THEN All (\h. RepUR ``cat-ob cat-arrow cat-id cat-comp name-cat type-cat`` h)⋅
   THEN Try (DProds)
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
CubicalSet  \mequiv{}  Functor(NameCat;TypeCat)


By

---

Latex:
((RepeatFor  2  (D  0)  THENA  Auto)
  THEN  RepeatFor  2  (D  1)
  THEN  Reduce  (-1)
  THEN  D  -1
  THEN  MemTypeCD
  THEN  All  (\mbackslash{}h.  RepUR  ``cat-ob  cat-arrow  cat-id  cat-comp  name-cat  type-cat``  h)\mcdot{}
  THEN  Try  (DProds)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index