Proof of Nuprl Lemma : Kan_sigma_filler

Step * 1 2 2 1 1 1 1 1 1 2 1 2 1 2 1 1 1 1 1 2 1 2 1 1 2 of Lemma Kan_sigma_filler_uniform

1. X : CubicalSet
2. A : {X ⊢ _(Kan)}
3. B : {X.Kan-type(A) ⊢ _(Kan)}
4. I : Cname List
5. alpha : X(I)
6. J : nameset(I) List
7. x : nameset(I)
8. i : ℕ2
9. bx : A-open-box(X;Σ Kan-type(A) Kan-type(B);I;alpha;J;x;i)
10. K : Cname List
11. f : name-morph(I;K)
12. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
13. ↑isname(f x)
14. map(f;J) ∈ nameset(K) List
15. f x ∈ nameset(K)
16. l_subset(Cname;map(f;J);K)
17. nameset([x / J]) ⊆r name-morph-domain(f;I)
18. (filler(x;i;sigma-box-fst(bx)) alpha f)
= filler(f x;i;A-open-box-image(X;Kan-type(A);I;K;f;alpha;sigma-box-fst(bx)))
∈ Kan-type(A)(f(alpha))
19. filler(f x;i;sigma-box-fst(A-open-box-image(X;Σ Kan-type(A) Kan-type(B);I;K;f;alpha;bx)))
= filler(f x;i;A-open-box-image(X;Kan-type(A);I;K;f;alpha;sigma-box-fst(bx)))
∈ Kan-type(A)(f(alpha))
20. cubeA : Kan-type(A)(f(alpha))

21. fills-A-open-box(X;Kan-type(A);K;f(alpha);sigma-box-fst(A-open-box-image(X;Σ Kan-type(A) ...;I;K;f;alpha;bx));cubeA)

22. cubeA1 : Kan-type(A)(alpha)
23. fills-A-open-box(X;Kan-type(A);I;alpha;sigma-box-fst(bx);cubeA1)
24. filler(x;i;sigma-box-fst(bx))
= cubeA1
∈ {cube:Kan-type(A)(alpha)| fills-A-open-box(X;Kan-type(A);I;alpha;sigma-box-fst(bx);cube)}
25. cubeA = (cubeA1 alpha f) ∈ Kan-type(A)(f(alpha))
26. (filler(x;i;sigma-box-snd(bx)) (alpha;cubeA1) f)
= filler(f x;i;A-open-box-image(X.Kan-type(A);Kan-type(B);I;K;f;(alpha;cubeA1);sigma-box-snd(bx)))
∈ Kan-type(B)(f((alpha;cubeA1)))
27. A-open-box-image(X;Σ Kan-type(A) Kan-type(B);I;K;f;alpha;bx)
    ∈ A-open-box(X;Σ Kan-type(A) Kan-type(B);K;f(alpha);map(f;J);f x;i)
28. sigma-box-snd(A-open-box-image(X;Σ Kan-type(A) Kan-type(B);I;K;f;alpha;bx))
    ∈ A-open-box(X.Kan-type(A);Kan-type(B);K;(f(alpha);cubeA);map(f;J);f x;i)
29. L : {fc:A-face(X;Σ Kan-type(A) Kan-type(B);I;alpha)| (fc ∈ bx)}  List
30. bx = L ∈ ({fc:A-face(X;Σ Kan-type(A) Kan-type(B);I;alpha)| (fc ∈ bx)}  List)
31. x2 : nameset(I)
32. i1 : ℕ2
33. u : Kan-type(A)((x2:=i1)(alpha))
34. x5 : Kan-type(B)(((x2:=i1)(alpha);u))
35. (<x2, i1, u, x5> ∈ bx)
36. f x2 ∈ nameset(K)
37. ↑isname(f x2)
38. u = (cubeA1 alpha (x2:=i1)) ∈ Kan-type(A)((x2:=i1)(alpha))
39. f ∈ name-morph(I-[x2];K-[f x2])

40. (cubeA f(alpha) (f x2:=i1)) = ((cubeA1 alpha f) f(alpha) (f x2:=i1)) ∈ Kan-type(A)((f x2:=i1)(f(alpha)))

41. ((cubeA1 alpha (x2:=i1)) (x2:=i1)(alpha) f) = (cubeA1 alpha ((x2:=i1) o f)) ∈ Kan-type(A)(((x2:=i1) o f)(alpha))

42. Kan-type(A)(f((x2:=i1)(alpha))) = Kan-type(A)((f x2:=i1)(f(alpha))) ∈ Type
⊢ ((cubeA1 alpha (x2:=i1)) (x2:=i1)(alpha) f)
= ((cubeA1 alpha f) f(alpha) (f x2:=i1))
∈ Kan-type(A)((f x2:=i1)(f(alpha)))
BY
{ (NthHypEq (-2) THEN EqCD) }

1
.....subterm..... T:t
1:n
1. X : CubicalSet
2. A : {X ⊢ _(Kan)}
3. B : {X.Kan-type(A) ⊢ _(Kan)}
4. I : Cname List
5. alpha : X(I)
6. J : nameset(I) List
7. x : nameset(I)
8. i : ℕ2
9. bx : A-open-box(X;Σ Kan-type(A) Kan-type(B);I;alpha;J;x;i)
10. K : Cname List
11. f : name-morph(I;K)
12. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
13. ↑isname(f x)
14. map(f;J) ∈ nameset(K) List
15. f x ∈ nameset(K)
16. l_subset(Cname;map(f;J);K)
17. nameset([x / J]) ⊆r name-morph-domain(f;I)
18. (filler(x;i;sigma-box-fst(bx)) alpha f)
= filler(f x;i;A-open-box-image(X;Kan-type(A);I;K;f;alpha;sigma-box-fst(bx)))
∈ Kan-type(A)(f(alpha))
19. filler(f x;i;sigma-box-fst(A-open-box-image(X;Σ Kan-type(A) Kan-type(B);I;K;f;alpha;bx)))
= filler(f x;i;A-open-box-image(X;Kan-type(A);I;K;f;alpha;sigma-box-fst(bx)))
∈ Kan-type(A)(f(alpha))
20. cubeA : Kan-type(A)(f(alpha))

21. fills-A-open-box(X;Kan-type(A);K;f(alpha);sigma-box-fst(A-open-box-image(X;Σ Kan-type(A) ...;I;K;f;alpha;bx));cubeA)

40. (cubeA f(alpha) (f x2:=i1)) = ((cubeA1 alpha f) f(alpha) (f x2:=i1)) ∈ Kan-type(A)((f x2:=i1)(f(alpha)))

41. ((cubeA1 alpha (x2:=i1)) (x2:=i1)(alpha) f) = (cubeA1 alpha ((x2:=i1) o f)) ∈ Kan-type(A)(((x2:=i1) o f)(alpha))

42. Kan-type(A)(f((x2:=i1)(alpha))) = Kan-type(A)((f x2:=i1)(f(alpha))) ∈ Type
⊢ Kan-type(A)((f x2:=i1)(f(alpha))) = Kan-type(A)(((x2:=i1) o f)(alpha)) ∈ Type

2
.....subterm..... T:t
2:n
1. X : CubicalSet
2. A : {X ⊢ _(Kan)}
3. B : {X.Kan-type(A) ⊢ _(Kan)}
4. I : Cname List
5. alpha : X(I)
6. J : nameset(I) List
7. x : nameset(I)
8. i : ℕ2
9. bx : A-open-box(X;Σ Kan-type(A) Kan-type(B);I;alpha;J;x;i)
10. K : Cname List
11. f : name-morph(I;K)
12. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
13. ↑isname(f x)
14. map(f;J) ∈ nameset(K) List
15. f x ∈ nameset(K)
16. l_subset(Cname;map(f;J);K)
17. nameset([x / J]) ⊆r name-morph-domain(f;I)
18. (filler(x;i;sigma-box-fst(bx)) alpha f)
= filler(f x;i;A-open-box-image(X;Kan-type(A);I;K;f;alpha;sigma-box-fst(bx)))
∈ Kan-type(A)(f(alpha))
19. filler(f x;i;sigma-box-fst(A-open-box-image(X;Σ Kan-type(A) Kan-type(B);I;K;f;alpha;bx)))
= filler(f x;i;A-open-box-image(X;Kan-type(A);I;K;f;alpha;sigma-box-fst(bx)))
∈ Kan-type(A)(f(alpha))
20. cubeA : Kan-type(A)(f(alpha))

21. fills-A-open-box(X;Kan-type(A);K;f(alpha);sigma-box-fst(A-open-box-image(X;Σ Kan-type(A) ...;I;K;f;alpha;bx));cubeA)

40. (cubeA f(alpha) (f x2:=i1)) = ((cubeA1 alpha f) f(alpha) (f x2:=i1)) ∈ Kan-type(A)((f x2:=i1)(f(alpha)))

41. ((cubeA1 alpha (x2:=i1)) (x2:=i1)(alpha) f) = (cubeA1 alpha ((x2:=i1) o f)) ∈ Kan-type(A)(((x2:=i1) o f)(alpha))

42. Kan-type(A)(f((x2:=i1)(alpha))) = Kan-type(A)((f x2:=i1)(f(alpha))) ∈ Type
⊢ ((cubeA1 alpha (x2:=i1)) (x2:=i1)(alpha) f)
= ((cubeA1 alpha (x2:=i1)) (x2:=i1)(alpha) f)
∈ Kan-type(A)((f x2:=i1)(f(alpha)))

3
.....subterm..... T:t
3:n
1. X : CubicalSet
2. A : {X ⊢ _(Kan)}
3. B : {X.Kan-type(A) ⊢ _(Kan)}
4. I : Cname List
5. alpha : X(I)
6. J : nameset(I) List
7. x : nameset(I)
8. i : ℕ2
9. bx : A-open-box(X;Σ Kan-type(A) Kan-type(B);I;alpha;J;x;i)
10. K : Cname List
11. f : name-morph(I;K)
12. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
13. ↑isname(f x)
14. map(f;J) ∈ nameset(K) List
15. f x ∈ nameset(K)
16. l_subset(Cname;map(f;J);K)
17. nameset([x / J]) ⊆r name-morph-domain(f;I)
18. (filler(x;i;sigma-box-fst(bx)) alpha f)
= filler(f x;i;A-open-box-image(X;Kan-type(A);I;K;f;alpha;sigma-box-fst(bx)))
∈ Kan-type(A)(f(alpha))
19. filler(f x;i;sigma-box-fst(A-open-box-image(X;Σ Kan-type(A) Kan-type(B);I;K;f;alpha;bx)))
= filler(f x;i;A-open-box-image(X;Kan-type(A);I;K;f;alpha;sigma-box-fst(bx)))
∈ Kan-type(A)(f(alpha))
20. cubeA : Kan-type(A)(f(alpha))

21. fills-A-open-box(X;Kan-type(A);K;f(alpha);sigma-box-fst(A-open-box-image(X;Σ Kan-type(A) ...;I;K;f;alpha;bx));cubeA)

40. (cubeA f(alpha) (f x2:=i1)) = ((cubeA1 alpha f) f(alpha) (f x2:=i1)) ∈ Kan-type(A)((f x2:=i1)(f(alpha)))

41. ((cubeA1 alpha (x2:=i1)) (x2:=i1)(alpha) f) = (cubeA1 alpha ((x2:=i1) o f)) ∈ Kan-type(A)(((x2:=i1) o f)(alpha))

42. Kan-type(A)(f((x2:=i1)(alpha))) = Kan-type(A)((f x2:=i1)(f(alpha))) ∈ Type

⊢ ((cubeA1 alpha f) f(alpha) (f x2:=i1)) = (cubeA1 alpha ((x2:=i1) o f)) ∈ Kan-type(A)((f x2:=i1)(f(alpha)))

4
.....antecedent.....
1. X : CubicalSet
2. A : {X ⊢ _(Kan)}
3. B : {X.Kan-type(A) ⊢ _(Kan)}
4. I : Cname List
5. alpha : X(I)
6. J : nameset(I) List
7. x : nameset(I)
8. i : ℕ2
9. bx : A-open-box(X;Σ Kan-type(A) Kan-type(B);I;alpha;J;x;i)
10. K : Cname List
11. f : name-morph(I;K)
12. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
13. ↑isname(f x)
14. map(f;J) ∈ nameset(K) List
15. f x ∈ nameset(K)
16. l_subset(Cname;map(f;J);K)
17. nameset([x / J]) ⊆r name-morph-domain(f;I)
18. (filler(x;i;sigma-box-fst(bx)) alpha f)
= filler(f x;i;A-open-box-image(X;Kan-type(A);I;K;f;alpha;sigma-box-fst(bx)))
∈ Kan-type(A)(f(alpha))
19. filler(f x;i;sigma-box-fst(A-open-box-image(X;Σ Kan-type(A) Kan-type(B);I;K;f;alpha;bx)))
= filler(f x;i;A-open-box-image(X;Kan-type(A);I;K;f;alpha;sigma-box-fst(bx)))
∈ Kan-type(A)(f(alpha))
20. cubeA : Kan-type(A)(f(alpha))

21. fills-A-open-box(X;Kan-type(A);K;f(alpha);sigma-box-fst(A-open-box-image(X;Σ Kan-type(A) ...;I;K;f;alpha;bx));cubeA)

40. (cubeA f(alpha) (f x2:=i1)) = ((cubeA1 alpha f) f(alpha) (f x2:=i1)) ∈ Kan-type(A)((f x2:=i1)(f(alpha)))

41. ((cubeA1 alpha (x2:=i1)) (x2:=i1)(alpha) f) = (cubeA1 alpha ((x2:=i1) o f)) ∈ Kan-type(A)(((x2:=i1) o f)(alpha))

42. Kan-type(A)(f((x2:=i1)(alpha))) = Kan-type(A)((f x2:=i1)(f(alpha))) ∈ Type
⊢ True

Latex:

Latex:
1. X : CubicalSet 2. A : \{X \mvdash{} \_(Kan)\} 3. B : \{X.Kan-type(A) \mvdash{} \_(Kan)\} 4. I : Cname List 5. alpha : X(I) 6. J : nameset(I) List 7. x : nameset(I) 8. i : \mBbbN{}2 9. bx : A-open-box(X;\mSigma{} Kan-type(A) Kan-type(B);I;alpha;J;x;i) 10. K : Cname List 11. f : name-morph(I;K) 12. \mforall{}i:nameset(I). ((i \mmember{} J) {}\mRightarrow{} (\muparrow{}isname(f i))) 13. \muparrow{}isname(f x) 14. map(f;J) \mmember{} nameset(K) List 15. f x \mmember{} nameset(K) 16. l\_subset(Cname;map(f;J);K) 17. nameset([x / J]) \msubseteq{}r name-morph-domain(f;I) 18. (filler(x;i;sigma-box-fst(bx)) alpha f) = filler(f x;i;A-open-box-image(X;Kan-type(A);I;K;f;alpha;sigma-box-fst(bx))) 19. filler(f x;i;sigma-box-fst(A-open-box-image(X;\mSigma{} Kan-type(A) Kan-type(B);I;K;f;alpha;bx))) = filler(f x;i;A-open-box-image(X;Kan-type(A);I;K;f;alpha;sigma-box-fst(bx))) 20. cubeA : Kan-type(A)(f(alpha)) 21. fills-A-open-box(X;Kan-type(A);K;f(alpha);sigma-box-fst(...);cubeA) 22. cubeA1 : Kan-type(A)(alpha) 23. fills-A-open-box(X;Kan-type(A);I;alpha;sigma-box-fst(bx);cubeA1) 24. filler(x;i;sigma-box-fst(bx)) = cubeA1 25. cubeA = (cubeA1 alpha f) 26. (filler(x;i;sigma-box-snd(bx)) (alpha;cubeA1) f) = filler(f x;i;A-open-box-image(X.Kan-type(A);Kan-type(B);I;K;f;(alpha;cubeA1);sigma-box-snd(bx))) 27. A-open-box-image(X;\mSigma{} Kan-type(A) Kan-type(B);I;K;f;alpha;bx) \mmember{} A-open-box(X;\mSigma{} Kan-type(A) Kan-type(B);K;f(alpha);map(f;J);f x;i) 28. sigma-box-snd(A-open-box-image(X;\mSigma{} Kan-type(A) Kan-type(B);I;K;f;alpha;bx)) \mmember{} A-open-box(X.Kan-type(A);Kan-type(B);K;(f(alpha);cubeA);map(f;J);f x;i) 29. L : \{fc:A-face(X;\mSigma{} Kan-type(A) Kan-type(B);I;alpha)| (fc \mmember{} bx)\} List 30. bx = L 31. x2 : nameset(I) 32. i1 : \mBbbN{}2 33. u : Kan-type(A)((x2:=i1)(alpha)) 34. x5 : Kan-type(B)(((x2:=i1)(alpha);u)) 35. (<x2, i1, u, x5> \mmember{} bx) 36. f x2 \mmember{} nameset(K) 37. \muparrow{}isname(f x2) 38. u = (cubeA1 alpha (x2:=i1)) 39. f \mmember{} name-morph(I-[x2];K-[f x2]) 40. (cubeA f(alpha) (f x2:=i1)) = ((cubeA1 alpha f) f(alpha) (f x2:=i1)) 41. ((cubeA1 alpha (x2:=i1)) (x2:=i1)(alpha) f) = (cubeA1 alpha ((x2:=i1) o f)) 42. Kan-type(A)(f((x2:=i1)(alpha))) = Kan-type(A)((f x2:=i1)(f(alpha))) \mvdash{} ((cubeA1 alpha (x2:=i1)) (x2:=i1)(alpha) f) = ((cubeA1 alpha f) f(alpha) (f x2:=i1)) By Latex: (NthHypEq (-2) THEN EqCD) Home Index