---

Step * of Lemma csm-Kan-unit-cube-comp

∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀x:{unit-cube(I) ⊢ _(Kan)}.
  ((x)unit-cube-map((f o g)) = ((x)unit-cube-map(f))unit-cube-map(g) ∈ {unit-cube(K) ⊢ _(Kan)})
BY
{ (Auto
   THEN Subst ⌜unit-cube-map((f o g)) = unit-cube-map(f) o unit-cube-map(g) ∈ unit-cube(K) ⟶ unit-cube(I)⌝ 0⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}I,J,K:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}g:name-morph(J;K).  \mforall{}x:\{unit-cube(I)  \mvdash{}  \_(Kan)\}.
    ((x)unit-cube-map((f  o  g))  =  ((x)unit-cube-map(f))unit-cube-map(g))


By

---

Latex:
(Auto  THEN  Subst  \mkleeneopen{}unit-cube-map((f  o  g))  =  unit-cube-map(f)  o  unit-cube-map(g)\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index