---

Step * of Lemma csm-Kan-cubical-identity

No Annotations
∀[X,Delta:CubicalSet]. ∀[s:Delta ⟶ X]. ∀[A:{X ⊢ _(Kan)}]. ∀[a,b:{X ⊢ _:Kan-type(A)}].
  ((Kan(Id_A a b))s = Kan(Id_(A)s (a)s (b)s) ∈ {Delta ⊢ _(Kan)})
BY
{ (Auto
   THEN BLemma `Kan-cubical-type-equal`
   THEN Auto
   THEN RW (AddrC [2] (UnfoldC `csm-Kan-cubical-type`)) 0
   THEN Unfold `Kan-cubical-identity` 0
   THEN Reduce 0
   THEN (Assert ((Id_Kan-type(A) a b))s = (Id_Kan-type((A)s) (a)s (b)s) ∈ {Delta ⊢ _} BY
               (BLemma `cubical-type-equal` THEN Auto))
   THEN EqCD
   THEN Auto) }

1
.....subterm..... T:t
2:n
1. X : CubicalSet
2. Delta : CubicalSet
3. s : Delta ⟶ X
4. A : {X ⊢ _(Kan)}
5. a : {X ⊢ _:Kan-type(A)}
6. b : {X ⊢ _:Kan-type(A)}
7. ((Id_Kan-type(A) a b))s = (Id_Kan-type((A)s) (a)s (b)s) ∈ {Delta ⊢ _}
⊢ (λI,alpha. (Kan_id_filler(X;A;a;b) I (s)alpha))
= Kan_id_filler(Delta;(A)s;(a)s;(b)s)
∈ (I:(Cname List)
  ⟶ alpha:Delta(I)
  ⟶ J:(nameset(I) List)
  ⟶ x:nameset(I)
  ⟶ i:ℕ2
  ⟶ A-open-box(Delta;((Id_Kan-type(A) a b))s;I;alpha;J;x;i)
  ⟶ ((Id_Kan-type(A) a b))s(alpha))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X,Delta:CubicalSet].  \mforall{}[s:Delta  {}\mrightarrow{}  X].  \mforall{}[A:\{X  \mvdash{}  \_(Kan)\}].  \mforall{}[a,b:\{X  \mvdash{}  \_:Kan-type(A)\}].
    ((Kan(Id\_A  a  b))s  =  Kan(Id\_(A)s  (a)s  (b)s))


By

---

Latex:
(Auto
  THEN  BLemma  `Kan-cubical-type-equal`
  THEN  Auto
  THEN  RW  (AddrC  [2]  (UnfoldC  `csm-Kan-cubical-type`))  0
  THEN  Unfold  `Kan-cubical-identity`  0
  THEN  Reduce  0
  THEN  (Assert  ((Id\_Kan-type(A)  a  b))s  =  (Id\_Kan-type((A)s)  (a)s  (b)s)  BY
                          (BLemma  `cubical-type-equal`  THEN  Auto))
  THEN  EqCD
  THEN  Auto)

---

Home Index