---

Step * of Lemma cubical-universe_wf

c𝕌 ∈ CubicalSet'
BY
{ (Unfold `cubical-universe` 0 THEN (MemTypeCD THENW Auto) THEN Reduce 0) }

1
<λI.{unit-cube(I) ⊢ _(Kan)}, λI,J,f,AK. (AK)unit-cube-map(f)> ∈ X:L:(Cname List) ⟶ 𝕌' × (I:(Cname List)
                                                                                ⟶ J:(Cname List)
                                                                                ⟶ name-morph(I;J)
                                                                                ⟶ (X I)
                                                                                ⟶ (X J))

2
(∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
   ((λAK.(AK)unit-cube-map((f o g)))
   = ((λAK.(AK)unit-cube-map(g)) o (λAK.(AK)unit-cube-map(f)))
   ∈ ({unit-cube(I) ⊢ _(Kan)} ⟶ {unit-cube(K) ⊢ _(Kan)})))
∧ (∀I:Cname List. ((λAK.(AK)unit-cube-map(1)) = (λx.x) ∈ ({unit-cube(I) ⊢ _(Kan)} ⟶ {unit-cube(I) ⊢ _(Kan)})))

---

Latex:

---

Latex:
c\mBbbU{}  \mmember{}  CubicalSet'


By

---

Latex:
(Unfold  `cubical-universe`  0  THEN  (MemTypeCD  THENW  Auto)  THEN  Reduce  0)

---

Home Index