---

Step * of Lemma unit-cube-map-comp

∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
  (unit-cube-map((f o g)) = unit-cube-map(f) o unit-cube-map(g) ∈ unit-cube(K) ⟶ unit-cube(I))
BY
{ ((Auto THEN InstLemma `cubical-set-is-functor` [])
   THEN RepUR ``cube-set-map`` 0
   THEN Symmetry
   THEN BLemma `nat-trans-equal`
   THEN Try (Fold `cube-set-map` 0)
   THEN Auto) }

1
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)))

---

Latex:

---

Latex:
\mforall{}I,J,K:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}g:name-morph(J;K).
    (unit-cube-map((f  o  g))  =  unit-cube-map(f)  o  unit-cube-map(g))


By

---

Latex:
((Auto  THEN  InstLemma  `cubical-set-is-functor`  [])
  THEN  RepUR  ``cube-set-map``  0
  THEN  Symmetry
  THEN  BLemma  `nat-trans-equal`
  THEN  Try  (Fold  `cube-set-map`  0)
  THEN  Auto)

---

Home Index