Proof of Nuprl Lemma : Kan_id_filler

Step * 2 2 1 1 1 1 1 2 1 1 1 2 2 1 1 2 1 3 1 of Lemma Kan_id_filler_wf

1. I : Cname List
2. X : CubicalSet
3. A : {X ⊢ _(Kan)}
4. a : {X ⊢ _:Kan-type(A)}
5. b : {X ⊢ _:Kan-type(A)}
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)
   ⟶ I-path(X;Kan-type(A);a;b;I;alpha)
7. 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)
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. ¬(fresh-cname(I) ∈ I-[x1])
22. v5 : named-path(X;Kan-type(A);a;b;I-[x1];(x1:=i1)(alpha);fresh-cname(I))
23. <fresh-cname(I), v5> = v3 ∈ (Id_Kan-type(A) a b)((x1:=i1)(alpha))
24. [fresh-cname(I) / I-[x1]] = [fresh-cname(I) / I]-[x1] ∈ (Cname List)

25. iota(fresh-cname(I))((x1:=i1)(alpha)) = (x1:=i1)(iota(fresh-cname(I))(alpha)) ∈ X([fresh-cname(I) / I-[x1]])

26. x2 : (v iota(fresh-cname(I))(alpha) (x1:=i1)) = v5 ∈ Kan-type(A)((x1:=i1)(iota(fresh-cname(I))(alpha)))
27. <fresh-cname(I), (v iota(fresh-cname(I))(alpha) (x1:=i1))> = v3 ∈ (Id_Kan-type(A) a b)((x1:=i1)(alpha))
28. ¬(fresh-cname(I-[x1]) ∈ I-[x1])

⊢ path-eq(X;Kan-type(A);I-[x1];(x1:=i1)(alpha);(<fresh-cname(I), v> alpha (x1:=i1));<fresh-cname(I), (v iota(fresh-cname\000C(I))(alpha) (x1:=i1))>)

BY
{ TACTIC:((RepUR ``path-eq named-path-morph`` 0
THEN (InstLemma `cubical-type-ap-morph-comp`

                 [⌜X⌝;⌜Kan-type(A)⌝;⌜[fresh-cname(I) / I]⌝;⌜[fresh-cname(I-[x1]) / I-[x1]]⌝;⌜[fresh-cname(I) / I-[x1]]⌝;

                 ⌜(x1:=i1)[fresh-cname(I):=fresh-cname(I-[x1])]⌝
                 ;⌜rename-one-name(fresh-cname(I-[x1]);fresh-cname(I))⌝
                 ;⌜iota(fresh-cname(I))(alpha)⌝; ⌜v⌝]⋅
                 THENA Auto
                 )
           )
          THEN TACTIC:(NthHypEq  (-1) THEN EqCD)
          ) }

1
.....subterm..... T:t
1:n
1. I : Cname List
2. X : CubicalSet
3. A : {X ⊢ _(Kan)}
4. a : {X ⊢ _:Kan-type(A)}
5. b : {X ⊢ _:Kan-type(A)}
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)
   ⟶ I-path(X;Kan-type(A);a;b;I;alpha)
7. 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)
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)

25. iota(fresh-cname(I))((x1:=i1)(alpha)) = (x1:=i1)(iota(fresh-cname(I))(alpha)) ∈ X([fresh-cname(I) / I-[x1]])

29. ((v iota(fresh-cname(I))(alpha) (x1:=i1)[fresh-cname(I):=fresh-cname(I-[x1])]) (x1:=i1)[...:=...](...(alpha)) ...)

= (v iota(fresh-cname(I))(alpha) ((x1:=i1)[fresh-cname(I):=fresh-cname(I-[x1])] o rename-one-name(...;fresh-cname(I))))

∈ Kan-type(A)(((x1:=i1)[fresh-cname(I):=fresh-cname(I-[x1])] o rename-one-name(fresh-cname(I-[x1]);...))(...(alpha)))

⊢ Kan-type(A)(iota(fresh-cname(I))((x1:=i1)(alpha)))
= Kan-type(A)(((x1:=i1)[fresh-cname(I):=fresh-cname(I-[x1])] o rename-one-name(fresh-cname(I-[x1]);...))(...(alpha)))
∈ Type

2
.....subterm..... T:t
2:n
1. I : Cname List
2. X : CubicalSet
3. A : {X ⊢ _(Kan)}
4. a : {X ⊢ _:Kan-type(A)}
5. b : {X ⊢ _:Kan-type(A)}
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)
   ⟶ I-path(X;Kan-type(A);a;b;I;alpha)
7. 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)
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)

25. iota(fresh-cname(I))((x1:=i1)(alpha)) = (x1:=i1)(iota(fresh-cname(I))(alpha)) ∈ X([fresh-cname(I) / I-[x1]])

29. ((v iota(fresh-cname(I))(alpha) (x1:=i1)[fresh-cname(I):=fresh-cname(I-[x1])]) (x1:=i1)[...:=...](...(alpha)) ...)

= (v iota(fresh-cname(I))(alpha) ((x1:=i1)[fresh-cname(I):=fresh-cname(I-[x1])] o rename-one-name(...;fresh-cname(I))))

∈ Kan-type(A)(((x1:=i1)[fresh-cname(I):=fresh-cname(I-[x1])] o rename-one-name(fresh-cname(I-[x1]);...))(...(alpha)))

⊢ ((v iota(fresh-cname(I))(alpha) (x1:=i1)[fresh-cname(I):=fresh-cname(I-[x1])]) iota(fresh-cname(I-[x1]))(...) ...)

= ((v iota(fresh-cname(I))(alpha) (x1:=i1)[fresh-cname(I):=fresh-cname(I-[x1])]) (x1:=i1)[fresh-cname(I):=...](...) ...)

∈ Kan-type(A)(iota(fresh-cname(I))((x1:=i1)(alpha)))

3
.....subterm..... T:t
3:n
1. I : Cname List
2. X : CubicalSet
3. A : {X ⊢ _(Kan)}
4. a : {X ⊢ _:Kan-type(A)}
5. b : {X ⊢ _:Kan-type(A)}
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)
   ⟶ I-path(X;Kan-type(A);a;b;I;alpha)
7. 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)
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)

25. iota(fresh-cname(I))((x1:=i1)(alpha)) = (x1:=i1)(iota(fresh-cname(I))(alpha)) ∈ X([fresh-cname(I) / I-[x1]])

29. ((v iota(fresh-cname(I))(alpha) (x1:=i1)[fresh-cname(I):=fresh-cname(I-[x1])]) (x1:=i1)[...:=...](...(alpha)) ...)

= (v iota(fresh-cname(I))(alpha) ((x1:=i1)[fresh-cname(I):=fresh-cname(I-[x1])] o rename-one-name(...;fresh-cname(I))))

∈ Kan-type(A)(((x1:=i1)[fresh-cname(I):=fresh-cname(I-[x1])] o rename-one-name(fresh-cname(I-[x1]);...))(...(alpha)))

⊢ (v iota(fresh-cname(I))(alpha) (x1:=i1))

= (v iota(fresh-cname(I))(alpha) ((x1:=i1)[fresh-cname(I):=fresh-cname(I-[x1])] o rename-one-name(...;fresh-cname(I))))

∈ Kan-type(A)(iota(fresh-cname(I))((x1:=i1)(alpha)))

4
.....antecedent.....
1. I : Cname List
2. X : CubicalSet
3. A : {X ⊢ _(Kan)}
4. a : {X ⊢ _:Kan-type(A)}
5. b : {X ⊢ _:Kan-type(A)}
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)
   ⟶ I-path(X;Kan-type(A);a;b;I;alpha)
7. 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)
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)

25. iota(fresh-cname(I))((x1:=i1)(alpha)) = (x1:=i1)(iota(fresh-cname(I))(alpha)) ∈ X([fresh-cname(I) / I-[x1]])

29. ((v iota(fresh-cname(I))(alpha) (x1:=i1)[fresh-cname(I):=fresh-cname(I-[x1])]) (x1:=i1)[...:=...](...(alpha)) ...)

= (v iota(fresh-cname(I))(alpha) ((x1:=i1)[fresh-cname(I):=fresh-cname(I-[x1])] o rename-one-name(...;fresh-cname(I))))

∈ Kan-type(A)(((x1:=i1)[fresh-cname(I):=fresh-cname(I-[x1])] o rename-one-name(fresh-cname(I-[x1]);...))(...(alpha)))

⊢ True

Latex:

Latex:
1. I : Cname List 2. X : CubicalSet 3. A : \{X \mvdash{} \_(Kan)\} 4. a : \{X \mvdash{} \_:Kan-type(A)\} 5. b : \{X \mvdash{} \_:Kan-type(A)\} 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{} I-path(X;Kan-type(A);a;b;I;alpha) 7. 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) 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> 21. \mneg{}(fresh-cname(I) \mmember{} I-[x1]) 22. v5 : named-path(X;Kan-type(A);a;b;I-[x1];(x1:=i1)(alpha);fresh-cname(I)) 23. <fresh-cname(I), v5> = v3 24. [fresh-cname(I) / I-[x1]] = [fresh-cname(I) / I]-[x1] 25. iota(fresh-cname(I))((x1:=i1)(alpha)) = (x1:=i1)(iota(fresh-cname(I))(alpha)) 26. x2 : (v iota(fresh-cname(I))(alpha) (x1:=i1)) = v5 27. <fresh-cname(I), (v iota(fresh-cname(I))(alpha) (x1:=i1))> = v3 28. \mneg{}(fresh-cname(I-[x1]) \mmember{} I-[x1]) \mvdash{} path-eq(X;Kan-type(A);I-[x1];(x1:=i1)(alpha);(<fresh-cname(I), v> alpha (x1:=i1));<fresh-cname(I),\000C (v iota(fresh-cname(I))(alpha) (x1:=i1))>) By Latex: TACTIC:((RepUR ``path-eq named-path-morph`` 0 THEN (InstLemma `cubical-type-ap-morph-comp` [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}Kan-type(A)\mkleeneclose{};\mkleeneopen{}[fresh-cname(I) / I]\mkleeneclose{};\mkleeneopen{}[fresh-cname(I-[x1]) / I-[x1]]\mkleeneclose{}; \mkleeneopen{}[fresh-cname(I) / I-[x1]]\mkleeneclose{};\mkleeneopen{}(x1:=i1)[fresh-cname(I):=fresh-cname(I-[x1])]\mkleeneclose{} ;\mkleeneopen{}rename-one-name(fresh-cname(I-[x1]);fresh-cname(I))\mkleeneclose{} ;\mkleeneopen{}iota(fresh-cname(I))(alpha)\mkleeneclose{}; \mkleeneopen{}v\mkleeneclose{}]\mcdot{} THENA Auto ) ) THEN TACTIC:(NthHypEq (-1) THEN EqCD) ) Home Index