---

Step * 1 of Lemma csm-Kan-comp


1. Gamma : CubicalSet
2. Delta : CubicalSet
3. Z : CubicalSet
4. s1 : Z ⟶ Delta
5. s2 : Delta ⟶ Gamma
6. AK : {Gamma ⊢ _(Kan)}
⊢ (AK)s2 o s1
= ((AK)s2)s1
∈ (A:{Z ⊢ _} × (I:(Cname List)
               ⟶ alpha:Z(I)
               ⟶ J:(nameset(I) List)
               ⟶ x:nameset(I)
               ⟶ i:ℕ2
               ⟶ A-open-box(Z;A;I;alpha;J;x;i)
               ⟶ A(alpha)))
BY
{ (D -1
   THEN D -2
   THEN RepUR ``csm-Kan-cubical-type`` 0
   THEN EqCD
   THEN Try ((RepeatFor 2 ((FunExt THENA Auto)) THEN Reduce 0 THEN EqCD))
   THEN Auto) }

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet
2.  Delta  :  CubicalSet
3.  Z  :  CubicalSet
4.  s1  :  Z  {}\mrightarrow{}  Delta
5.  s2  :  Delta  {}\mrightarrow{}  Gamma
6.  AK  :  \{Gamma  \mvdash{}  \_(Kan)\}
\mvdash{}  (AK)s2  o  s1  =  ((AK)s2)s1


By

---

Latex:
(D  -1
  THEN  D  -2
  THEN  RepUR  ``csm-Kan-cubical-type``  0
  THEN  EqCD
  THEN  Try  ((RepeatFor  2  ((FunExt  THENA  Auto))  THEN  Reduce  0  THEN  EqCD))
  THEN  Auto)

---

Home Index