---

Step * 2 of Lemma cubical-universe_wf


(∀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)})))
BY
{ Auto }

---

Latex:

---

Latex:

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


By

---

Latex:
Auto

---

Home Index