---

Step * 2 2 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)
⊢ fills-A-open-box(X;(Id_Kan-type(A) a b);I;alpha;bx;Kan_id_filler(X;A;a;b) I alpha J x i bx)
BY
{ TACTIC:(Assert name-path-endpoints(X;Kan-type(A);a;b;I;alpha;fresh-cname(I);filler(x;i;...)) BY
                ((Assert Kan_id_filler(X;A;a;b) I alpha J x i bx ∈ I-path(X;Kan-type(A);a;b;I;alpha) BY
                        (Thin 6 THEN Auto))
                 THEN RepUR ``Kan_id_filler I-path`` -1
                 THEN (MemHD (-1) THENA Auto)
                 THEN All Reduce
                 THEN (MemTypeHD (-1) THENA Auto)
                 THEN ((D 0 THEN D -1 THEN Hypothesis) ORELSE (GenConclTerm ⌜fresh-cname(I)⌝⋅ THEN Auto)))) }

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. name-path-endpoints(X;Kan-type(A);a;b;I;alpha;fresh-cname(I);filler(x;i;cubical-id-box(X;Kan-type(A);a;b;I;...;bx)))
⊢ fills-A-open-box(X;(Id_Kan-type(A) a b);I;alpha;bx;Kan_id_filler(X;A;a;b) I alpha J x i bx)

---

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)
\mvdash{}  fills-A-open-box(X;(Id\_Kan-type(A)  a  b);I;alpha;bx;Kan\_id\_filler(X;A;a;b)  I  alpha  J  x  i  bx)


By

---

Latex:
TACTIC:(Assert  name-path-endpoints(X;Kan-type(A);a;b;I;alpha;fresh-cname(I);filler(x;i;...))  BY
                            ((Assert  Kan\_id\_filler(X;A;a;b)  I  alpha  J  x  i  bx
                                              \mmember{}  I-path(X;Kan-type(A);a;b;I;alpha)  BY
                                            (Thin  6  THEN  Auto))
                              THEN  RepUR  ``Kan\_id\_filler  I-path``  -1
                              THEN  (MemHD  (-1)  THENA  Auto)
                              THEN  All  Reduce
                              THEN  (MemTypeHD  (-1)  THENA  Auto)
                              THEN  ((D  0  THEN  D  -1  THEN  Hypothesis)
                              ORELSE  (GenConclTerm  \mkleeneopen{}fresh-cname(I)\mkleeneclose{}\mcdot{}  THEN  Auto)
                              )))

---

Home Index