---

Step * of Lemma csm-Kan-comp

∀[Gamma,Delta,Z:CubicalSet]. ∀[s1:Z ⟶ Delta]. ∀[s2:Delta ⟶ Gamma]. ∀[AK:{Gamma ⊢ _(Kan)}].
  ((AK)s2 o s1 = ((AK)s2)s1 ∈ {Z ⊢ _(Kan)})
BY
{ (Auto THEN BLemma `Kan-cubical-type-equal` THEN Auto) }

1
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)))

---

Latex:

---

Latex:
\mforall{}[Gamma,Delta,Z:CubicalSet].  \mforall{}[s1:Z  {}\mrightarrow{}  Delta].  \mforall{}[s2:Delta  {}\mrightarrow{}  Gamma].  \mforall{}[AK:\{Gamma  \mvdash{}  \_(Kan)\}].
    ((AK)s2  o  s1  =  ((AK)s2)s1)


By

---

Latex:
(Auto  THEN  BLemma  `Kan-cubical-type-equal`  THEN  Auto)

---

Home Index