---

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


1. I : Cname List
2. CubicalSet ≡ Functor(NameCat;TypeCat)
⊢ 1(unit-cube(I))
= unit-cube-map(1)
∈ (A:cat-ob(NameCat) ⟶ (cat-arrow(TypeCat) (ob(unit-cube(I)) A) (ob(unit-cube(I)) A)))
BY
{ (FunExt THENA Auto) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(FunExt  THENA  Auto)

---

Home Index