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