---

Step * 1 of Lemma unit-cube-map-comp


1. I : Cname List
2. J : Cname List
3. K : Cname List
4. f : name-morph(I;J)
5. g : name-morph(J;K)
6. CubicalSet ≡ Functor(NameCat;TypeCat)
⊢ unit-cube-map(f) o unit-cube-map(g)
= unit-cube-map((f o g))
∈ (A:cat-ob(NameCat) ⟶ (cat-arrow(TypeCat) (ob(unit-cube(K)) A) (ob(unit-cube(I)) A)))
BY
{ (RepUR ``name-cat type-cat cat-ob cat-arrow functor-ob unit-cube unit-cube-map csm-comp`` 0
   THEN RepUR ``trans-comp cat-comp compose`` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  J  :  Cname  List
3.  K  :  Cname  List
4.  f  :  name-morph(I;J)
5.  g  :  name-morph(J;K)
6.  CubicalSet  \mequiv{}  Functor(NameCat;TypeCat)
\mvdash{}  unit-cube-map(f)  o  unit-cube-map(g)  =  unit-cube-map((f  o  g))


By

---

Latex:
(RepUR  ``name-cat  type-cat  cat-ob  cat-arrow  functor-ob  unit-cube  unit-cube-map  csm-comp``  0
  THEN  RepUR  ``trans-comp  cat-comp  compose``  0
  THEN  Auto)

---

Home Index