---

Step * 2 2 1 1 1 1 of Lemma Kan_id_filler_wf


1. X : CubicalSet
2. A : {X ⊢ _(Kan)}
3. a : {X ⊢ _:Kan-type(A)}
4. b : {X ⊢ _:Kan-type(A)}
5. Kan_id_filler(X;A;a;b) ∈ I:(Cname List)
   ⟶ alpha:X(I)
   ⟶ J:(nameset(I) List)
   ⟶ x:nameset(I)
   ⟶ i:ℕ2
   ⟶ A-open-box(X;(Id_Kan-type(A) a b);I;alpha;J;x;i)
   ⟶ I-path(X;Kan-type(A);a;b;I;alpha)
6. Kan_id_filler(X;A;a;b) ∈ I:(Cname List)
   ⟶ alpha:X(I)
   ⟶ J:(nameset(I) List)
   ⟶ x:nameset(I)
   ⟶ i:ℕ2
   ⟶ A-open-box(X;(Id_Kan-type(A) a b);I;alpha;J;x;i)
   ⟶ (Id_Kan-type(A) a b)(alpha)
7. I : Cname List
8. alpha : X(I)
9. J : nameset(I) List
10. x : nameset(I)
11. i : ℕ2
12. bx : A-open-box(X;(Id_Kan-type(A) a b);I;alpha;J;x;i)
13. v : Kan-type(A)(iota(fresh-cname(I))(alpha))
14. fills-A-open-box(X;Kan-type(A);[fresh-cname(I) / 
                                    I];iota(fresh-cname(I))(alpha);cubical-id-box(X;Kan-type(A);a;b;I;alpha;bx);v)
15. name-path-endpoints(X;Kan-type(A);a;b;I;alpha;fresh-cname(I);v)
16. j : ℕ||bx||
17. x1 : nameset(I)
18. i1 : ℕ2
19. v3 : (Id_Kan-type(A) a b)((x1:=i1)(alpha))
20. bx[j] = <x1, i1, v3> ∈ A-face(X;(Id_Kan-type(A) a b);I;alpha)
⊢ (<fresh-cname(I), v> alpha (x1:=i1)) = v3 ∈ (Id_Kan-type(A) a b)((x1:=i1)(alpha))
BY
{ OnMaybeHyp 14 (\h. (DupHyp h
                      THEN RepUR ``fills-A-open-box fills-A-faces cubical-id-box extend-A-open-box lift-id-faces`` -1
                      THEN (With ⌜j + 2⌝ (D (-1))⋅
                            THENA ((Reduce 0 THEN (RWO "length-map" 0 THENA Auto)) THEN All Thin THEN Auto)
                            )
                      THEN RepeatFor 2 ((RWO "select-cons-tl" (-1) THEN Auto))
                      THEN RWO  "select-map" (-1)
                      THEN Auto
                      THEN (Subst' (j + 2) - 1 - 1 ~ j -1 THENA Auto)
                      THEN Reduce (-1))) }

1
1. X : CubicalSet
2. A : {X ⊢ _(Kan)}
3. a : {X ⊢ _:Kan-type(A)}
4. b : {X ⊢ _:Kan-type(A)}
5. Kan_id_filler(X;A;a;b) ∈ I:(Cname List)
   ⟶ alpha:X(I)
   ⟶ J:(nameset(I) List)
   ⟶ x:nameset(I)
   ⟶ i:ℕ2
   ⟶ A-open-box(X;(Id_Kan-type(A) a b);I;alpha;J;x;i)
   ⟶ I-path(X;Kan-type(A);a;b;I;alpha)
6. Kan_id_filler(X;A;a;b) ∈ I:(Cname List)
   ⟶ alpha:X(I)
   ⟶ J:(nameset(I) List)
   ⟶ x:nameset(I)
   ⟶ i:ℕ2
   ⟶ A-open-box(X;(Id_Kan-type(A) a b);I;alpha;J;x;i)
   ⟶ (Id_Kan-type(A) a b)(alpha)
7. I : Cname List
8. alpha : X(I)
9. J : nameset(I) List
10. x : nameset(I)
11. i : ℕ2
12. bx : A-open-box(X;(Id_Kan-type(A) a b);I;alpha;J;x;i)
13. v : Kan-type(A)(iota(fresh-cname(I))(alpha))
14. fills-A-open-box(X;Kan-type(A);[fresh-cname(I) / 
                                    I];iota(fresh-cname(I))(alpha);cubical-id-box(X;Kan-type(A);a;b;I;alpha;bx);v)
15. name-path-endpoints(X;Kan-type(A);a;b;I;alpha;fresh-cname(I);v)
16. j : ℕ||bx||
17. x1 : nameset(I)
18. i1 : ℕ2
19. v3 : (Id_Kan-type(A) a b)((x1:=i1)(alpha))
20. bx[j] = <x1, i1, v3> ∈ A-face(X;(Id_Kan-type(A) a b);I;alpha)
21. is-A-face(X;Kan-type(A);[fresh-cname(I) / 
                             I];iota(fresh-cname(I))(alpha);v;lift-id-face(X;Kan-type(A);I;alpha;bx[j]))
⊢ (<fresh-cname(I), v> alpha (x1:=i1)) = v3 ∈ (Id_Kan-type(A) a b)((x1:=i1)(alpha))

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  A  :  \{X  \mvdash{}  \_(Kan)\}
3.  a  :  \{X  \mvdash{}  \_:Kan-type(A)\}
4.  b  :  \{X  \mvdash{}  \_:Kan-type(A)\}
5.  Kan\_id\_filler(X;A;a;b)  \mmember{}  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;(Id\_Kan-type(A)  a  b);I;alpha;J;x;i)
      {}\mrightarrow{}  I-path(X;Kan-type(A);a;b;I;alpha)
6.  Kan\_id\_filler(X;A;a;b)  \mmember{}  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;(Id\_Kan-type(A)  a  b);I;alpha;J;x;i)
      {}\mrightarrow{}  (Id\_Kan-type(A)  a  b)(alpha)
7.  I  :  Cname  List
8.  alpha  :  X(I)
9.  J  :  nameset(I)  List
10.  x  :  nameset(I)
11.  i  :  \mBbbN{}2
12.  bx  :  A-open-box(X;(Id\_Kan-type(A)  a  b);I;alpha;J;x;i)
13.  v  :  Kan-type(A)(iota(fresh-cname(I))(alpha))
14.  fills-A-open-box(X;Kan-type(A);[fresh-cname(I)  / 
                                                                        I];iota(fresh-cname(I))(alpha);...;v)
15.  name-path-endpoints(X;Kan-type(A);a;b;I;alpha;fresh-cname(I);v)
16.  j  :  \mBbbN{}||bx||
17.  x1  :  nameset(I)
18.  i1  :  \mBbbN{}2
19.  v3  :  (Id\_Kan-type(A)  a  b)((x1:=i1)(alpha))
20.  bx[j]  =  <x1,  i1,  v3>
\mvdash{}  (<fresh-cname(I),  v>  alpha  (x1:=i1))  =  v3


By

---

Latex:
OnMaybeHyp  14  (\mbackslash{}h.
(DupHyp  h
  THEN  RepUR  ``fills-A-open-box  fills-A-faces  cubical-id-box  extend-A-open-box  lift-id-faces``  -1
  THEN  (With  \mkleeneopen{}j  +  2\mkleeneclose{}  (D  (-1))\mcdot{}
              THENA  ((Reduce  0  THEN  (RWO  "length-map"  0  THENA  Auto))  THEN  All  Thin  THEN  Auto)
              )
  THEN  RepeatFor  2  ((RWO  "select-cons-tl"  (-1)  THEN  Auto))
  THEN  RWO    "select-map"  (-1)
  THEN  Auto
  THEN  (Subst'  (j  +  2)  -  1  -  1  \msim{}  j  -1  THENA  Auto)
  THEN  Reduce  (-1)))

---

Home Index