---

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

.....wf..... 
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(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
{ TACTIC:(InstLemma `cubical-id-box_wf` [⌜Delta⌝;⌜(A1)s⌝;⌜(a)s⌝;⌜(b)s⌝;⌜I⌝;⌜J⌝;⌜x⌝;⌜i⌝;⌜alpha⌝;⌜x1⌝]⋅ THENA Auto) }

1
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)
19. cubical-id-box(Delta;(A1)s;(a)s;(b)s;I;alpha;x1)
    ∈ A-open-box(Delta;(A1)s;[fresh-cname(I) / I];iota(fresh-cname(I))(alpha);[fresh-cname(I) / J];x;i)
⊢ 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

---

Latex:

---

Latex:
.....wf..... 
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(Delta;(A1)s;(a)s;(b)s;I;alpha;x1)
    \mmember{}  A-face(X;A1;[fresh-cname(I)  /  I];iota(fresh-cname(I))((s)alpha))  List


By

---

Latex:
TACTIC:(InstLemma  `cubical-id-box\_wf`  [\mkleeneopen{}Delta\mkleeneclose{};\mkleeneopen{}(A1)s\mkleeneclose{};\mkleeneopen{}(a)s\mkleeneclose{};\mkleeneopen{}(b)s\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}alpha\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{}]\mcdot{}
                THENA  Auto
                )

---

Home Index