---

Step * 1 1 1 2 1 2 of Lemma csm-Kan-cubical-identity


1. X : CubicalSet
2. Delta : CubicalSet
3. s : Delta ⟶ X
4. A1 : {X ⊢ _}
5. A2 : I:(Cname List)
⟶ alpha:X(I)
⟶ J:(nameset(I) List)
⟶ x:nameset(I)
⟶ i:ℕ2
⟶ A-open-box(X;A1;I;alpha;J;x;i)
⟶ A1(alpha)
6. let A,filler = <A1, A2> 
   in Kan-A-filler(X;A;filler) ∧ uniform-Kan-A-filler(X;A;filler)
7. a : {X ⊢ _:A1}
8. b : {X ⊢ _:A1}
9. ((Id_A1 a b))s = (Id_(A1)s (a)s (b)s) ∈ {Delta ⊢ _}
10. I : Cname List
11. alpha : Delta(I)
12. J : nameset(I) List
13. x : nameset(I)
14. i : ℕ2
15. x1 : A-open-box(Delta;((Id_A1 a b))s;I;alpha;J;x;i)
16. A-open-box(Delta;((Id_A1 a b))s;I;alpha;J;x;i) ⊆r A-open-box(X;(Id_A1 a b);I;(s)alpha;J;x;i)
17. <fresh-cname(I)
    , A2 [fresh-cname(I) / I] iota(fresh-cname(I))((s)alpha) [fresh-cname(I) / J] x i 
      cubical-id-box(X;A1;a;b;I;(s)alpha;x1)
    > ∈ I-path(X;A1;a;b;I;(s)alpha)
18. <fresh-cname(I)
    , A2 [fresh-cname(I) / I] (s)iota(fresh-cname(I))(alpha) [fresh-cname(I) / J] x i 
      cubical-id-box(Delta;(A1)s;(a)s;(b)s;I;alpha;x1)
    > ∈ I-path(X;A1;a;b;I;(s)alpha)
⊢ cubical-id-box(X;A1;a;b;I;(s)alpha;x1)
= cubical-id-box(Delta;(A1)s;(a)s;(b)s;I;alpha;x1)
∈ (A-face(X;A1;[fresh-cname(I) / I];iota(fresh-cname(I))((s)alpha)) List)
BY
{ (RepUR ``cubical-id-box extend-A-open-box`` 0 THEN EqCDA) }

1
.....subterm..... T:t
1:n
1. X : CubicalSet
2. Delta : CubicalSet
3. s : Delta ⟶ X
4. A1 : {X ⊢ _}
5. A2 : I:(Cname List)
⟶ alpha:X(I)
⟶ J:(nameset(I) List)
⟶ x:nameset(I)
⟶ i:ℕ2
⟶ A-open-box(X;A1;I;alpha;J;x;i)
⟶ A1(alpha)
6. let A,filler = <A1, A2> 
   in Kan-A-filler(X;A;filler) ∧ uniform-Kan-A-filler(X;A;filler)
7. a : {X ⊢ _:A1}
8. b : {X ⊢ _:A1}
9. ((Id_A1 a b))s = (Id_(A1)s (a)s (b)s) ∈ {Delta ⊢ _}
10. I : Cname List
11. alpha : Delta(I)
12. J : nameset(I) List
13. x : nameset(I)
14. i : ℕ2
15. x1 : A-open-box(Delta;((Id_A1 a b))s;I;alpha;J;x;i)
16. A-open-box(Delta;((Id_A1 a b))s;I;alpha;J;x;i) ⊆r A-open-box(X;(Id_A1 a b);I;(s)alpha;J;x;i)
17. <fresh-cname(I)
    , A2 [fresh-cname(I) / I] iota(fresh-cname(I))((s)alpha) [fresh-cname(I) / J] x i 
      cubical-id-box(X;A1;a;b;I;(s)alpha;x1)
    > ∈ I-path(X;A1;a;b;I;(s)alpha)
18. <fresh-cname(I)
    , A2 [fresh-cname(I) / I] (s)iota(fresh-cname(I))(alpha) [fresh-cname(I) / J] x i 
      cubical-id-box(Delta;(A1)s;(a)s;(b)s;I;alpha;x1)
    > ∈ I-path(X;A1;a;b;I;(s)alpha)
⊢ term-A-face(a;I;(s)alpha;0)
= term-A-face((a)s;I;alpha;0)
∈ A-face(X;A1;[fresh-cname(I) / I];iota(fresh-cname(I))((s)alpha))

2
.....subterm..... T:t
2:n
1. X : CubicalSet
2. Delta : CubicalSet
3. s : Delta ⟶ X
4. A1 : {X ⊢ _}
5. A2 : I:(Cname List)
⟶ alpha:X(I)
⟶ J:(nameset(I) List)
⟶ x:nameset(I)
⟶ i:ℕ2
⟶ A-open-box(X;A1;I;alpha;J;x;i)
⟶ A1(alpha)
6. let A,filler = <A1, A2> 
   in Kan-A-filler(X;A;filler) ∧ uniform-Kan-A-filler(X;A;filler)
7. a : {X ⊢ _:A1}
8. b : {X ⊢ _:A1}
9. ((Id_A1 a b))s = (Id_(A1)s (a)s (b)s) ∈ {Delta ⊢ _}
10. I : Cname List
11. alpha : Delta(I)
12. J : nameset(I) List
13. x : nameset(I)
14. i : ℕ2
15. x1 : A-open-box(Delta;((Id_A1 a b))s;I;alpha;J;x;i)
16. A-open-box(Delta;((Id_A1 a b))s;I;alpha;J;x;i) ⊆r A-open-box(X;(Id_A1 a b);I;(s)alpha;J;x;i)
17. <fresh-cname(I)
    , A2 [fresh-cname(I) / I] iota(fresh-cname(I))((s)alpha) [fresh-cname(I) / J] x i 
      cubical-id-box(X;A1;a;b;I;(s)alpha;x1)
    > ∈ I-path(X;A1;a;b;I;(s)alpha)
18. <fresh-cname(I)
    , A2 [fresh-cname(I) / I] (s)iota(fresh-cname(I))(alpha) [fresh-cname(I) / J] x i 
      cubical-id-box(Delta;(A1)s;(a)s;(b)s;I;alpha;x1)
    > ∈ I-path(X;A1;a;b;I;(s)alpha)
⊢ [term-A-face(b;I;(s)alpha;1) / lift-id-faces(X;A1;I;(s)alpha;x1)]
= [term-A-face((b)s;I;alpha;1) / lift-id-faces(Delta;(A1)s;I;alpha;x1)]
∈ (A-face(X;A1;[fresh-cname(I) / I];iota(fresh-cname(I))((s)alpha)) List)

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  Delta  :  CubicalSet
3.  s  :  Delta  {}\mrightarrow{}  X
4.  A1  :  \{X  \mvdash{}  \_\}
5.  A2  :  I:(Cname  List)
{}\mrightarrow{}  alpha:X(I)
{}\mrightarrow{}  J:(nameset(I)  List)
{}\mrightarrow{}  x:nameset(I)
{}\mrightarrow{}  i:\mBbbN{}2
{}\mrightarrow{}  A-open-box(X;A1;I;alpha;J;x;i)
{}\mrightarrow{}  A1(alpha)
6.  let  A,filler  =  <A1,  A2> 
      in  Kan-A-filler(X;A;filler)  \mwedge{}  uniform-Kan-A-filler(X;A;filler)
7.  a  :  \{X  \mvdash{}  \_:A1\}
8.  b  :  \{X  \mvdash{}  \_:A1\}
9.  ((Id\_A1  a  b))s  =  (Id\_(A1)s  (a)s  (b)s)
10.  I  :  Cname  List
11.  alpha  :  Delta(I)
12.  J  :  nameset(I)  List
13.  x  :  nameset(I)
14.  i  :  \mBbbN{}2
15.  x1  :  A-open-box(Delta;((Id\_A1  a  b))s;I;alpha;J;x;i)
16.  A-open-box(Delta;((Id\_A1  a  b))s;I;alpha;J;x;i)  \msubseteq{}r  A-open-box(X;(Id\_A1  a  b);I;(s)alpha;J;x;i)
17.  <fresh-cname(I)
        ,  A2  [fresh-cname(I)  /  I]  iota(fresh-cname(I))((s)alpha)  [fresh-cname(I)  /  J]  x  i 
            cubical-id-box(X;A1;a;b;I;(s)alpha;x1)
        >  \mmember{}  I-path(X;A1;a;b;I;(s)alpha)
18.  <fresh-cname(I)
        ,  A2  [fresh-cname(I)  /  I]  (s)iota(fresh-cname(I))(alpha)  [fresh-cname(I)  /  J]  x  i 
            cubical-id-box(Delta;(A1)s;(a)s;(b)s;I;alpha;x1)
        >  \mmember{}  I-path(X;A1;a;b;I;(s)alpha)
\mvdash{}  cubical-id-box(X;A1;a;b;I;(s)alpha;x1)  =  cubical-id-box(Delta;(A1)s;(a)s;(b)s;I;alpha;x1)


By

---

Latex:
(RepUR  ``cubical-id-box  extend-A-open-box``  0  THEN  EqCDA)

---

Home Index