---

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


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))
BY
{ (FunExt THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  CubicalSet  \mequiv{}  Functor(<Cname  List,  \mlambda{}I,J.  name-morph(I;J),  \mlambda{}I.1,  \mlambda{}I,J,K,f,g.  (f  o  g)>TypeCat)
3.  A  :  Cname  List
\mvdash{}  (\mlambda{}x.x)  =  (\mlambda{}g.(1  o  g))


By

---

Latex:
(FunExt  THEN  Reduce  0  THEN  Auto)

---

Home Index