---

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


1. I : Cname List
2. CubicalSet ≡ Functor(NameCat;TypeCat)
3. A : cat-ob(NameCat)
⊢ (1(unit-cube(I)) A) = (unit-cube-map(1) A) ∈ (cat-arrow(TypeCat) (ob(unit-cube(I)) A) (ob(unit-cube(I)) A))
BY
{ (All (RepUR ``cat-ob name-cat unit-cube unit-cube-map csm-id identity-trans``)⋅
   THEN RepUR ``cat-id cat-arrow type-cat functor-ob`` 0
   ) }

1
1. I : Cname List
2. CubicalSet ≡ Functor(<Cname List, λI,J. name-morph(I;J), λI.1, λI,J,K,f,g. (f o g)>;TypeCat)
3. A : Cname List
⊢ (λx.x) = (λg.(1 o g)) ∈ (name-morph(I;A) ⟶ name-morph(I;A))

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  CubicalSet  \mequiv{}  Functor(NameCat;TypeCat)
3.  A  :  cat-ob(NameCat)
\mvdash{}  (1(unit-cube(I))  A)  =  (unit-cube-map(1)  A)


By

---

Latex:
(All  (RepUR  ``cat-ob  name-cat  unit-cube  unit-cube-map  csm-id  identity-trans``)\mcdot{}
  THEN  RepUR  ``cat-id  cat-arrow  type-cat  functor-ob``  0
  )

---

Home Index