Step
*
1
1
1
1
1
2
2
2
1
1
2
2
1
2
1
1
1
1
2
1
2
1
1
1
1
1
2
1
2
2
2
1
1
1
of Lemma
glue-comp-agrees
.....assertion.....
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. cA : G +⊢ Compositon(A)
4. phi : {G ⊢ _:𝔽}
5. T : {G, phi ⊢ _}
6. cT : composition-function{[i | j]:l, i:l}(G, phi; T)
7. uniform-comp-function{[i | j]:l, i:l}(G, phi; T; cT)
8. f : {G, phi ⊢ _:Equiv(T;A)}
9. H : CubicalSet{j}
10. sigma : H.𝕀 j⟶ G, phi
11. psi : {H ⊢ _:𝔽}
12. b : {H, psi.𝕀 ⊢ _:(T)sigma}
13. b0 : {H ⊢ _:((T)sigma)[0(𝕀)][psi |⟶ (b)[0(𝕀)]]}
14. G ⊢ Glue [phi ⊢→ (T;equiv-fun(f))] A
15. (Glue [phi ⊢→ (T;equiv-fun(f))] A)sigma
= H.𝕀 ⊢ Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma
∈ {H.𝕀 ⊢ _}
16. (T)sigma = H.𝕀 ⊢ Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma ∈ {H.𝕀 ⊢ _}
17. {H.𝕀 ⊢ _:Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma} = {H.𝕀 ⊢ _:(T)sigma} ∈ 𝕌{[i' | j']}
18. {b ∈ {H.𝕀, (psi)p ⊢ _:Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma}}
19. (phi)sigma = 1(𝔽) ∈ {H.𝕀 ⊢ _:𝔽}
20. (equiv-fun(f))sigma ∈ {H.𝕀 ⊢ _:((T ⟶ A))sigma}
21. (equiv-fun(f))sigma ∈ {H.𝕀 ⊢ _:((T)sigma ⟶ (A)sigma)}
22. H ⊢ ((T)sigma)[0(𝕀)]
23. ((equiv-fun(f))sigma)[0(𝕀)] ∈ {H ⊢ _:(((T ⟶ A))sigma)[0(𝕀)]}
24. ((equiv-fun(f))sigma)[0(𝕀)] ∈ {H ⊢ _:(((T)sigma)[0(𝕀)] ⟶ ((A)sigma)[0(𝕀)])}
25. ((phi)sigma)[0(𝕀)] = 1(𝔽) ∈ {H ⊢ _:𝔽}
26. app((equiv-fun(f))sigma; b) ∈ {H.𝕀, (psi)p ⊢ _:(A)sigma}
27. a : {H.𝕀, (psi)p ⊢ _:(A)sigma}
28. unglue(b) = a ∈ {H.𝕀, (psi)p ⊢ _:(A)sigma}
29. a = app((equiv-fun(f))sigma; b) ∈ {H.𝕀, (psi)p ⊢ _:(A)sigma}
30. a0 : {H ⊢ _:((A)sigma)[0(𝕀)]}
31. unglue(b0) = a0 ∈ {H ⊢ _:((A)sigma)[0(𝕀)]}
32. a0 = app(((equiv-fun(f))sigma)[0(𝕀)]; b0) ∈ {H ⊢ _:((A)sigma)[0(𝕀)]}
33. a0 ∈ {H ⊢ _:((A)sigma)[0(𝕀)][psi |⟶ a[0]]}
34. comp (cA)sigma [psi ⊢→ a] a0 ∈ {H ⊢ _:((A)sigma)[1(𝕀)][psi |⟶ a[1]]}
35. a'1 : {H ⊢ _:((A)sigma)[1(𝕀)][psi |⟶ a[1]]}
36. comp (cA)sigma [psi ⊢→ a] a0 = a'1 ∈ {H ⊢ _:((A)sigma)[1(𝕀)][psi |⟶ a[1]]}
37. (H ⊢ ∀ (phi)sigma) = 1(𝔽) ∈ {H ⊢ _:𝔽}
38. xx : {H ⊢ _:((T)sigma)[1(𝕀)]}
39. (cT H sigma psi b b0) = xx ∈ {H ⊢ _:((T)sigma)[1(𝕀)]}
40. t'1 : {H ⊢ _:((T)sigma)[1(𝕀)]}
41. comp (cT)sigma [psi ⊢→ b] b0 = t'1 ∈ {H ⊢ _:((T)sigma)[1(𝕀)]}
42. xx = t'1 ∈ {H ⊢ _:((T)sigma)[1(𝕀)]}
43. tt'1 : {H ⊢ _:((T)sigma)[1(𝕀)]}
44. tt'1 = t'1 ∈ {H ⊢ _:((T)sigma)[1(𝕀)]}
45. (equiv-fun(f))sigma ∈ {H, (∀ (phi)sigma).𝕀 ⊢ _:((T)sigma ⟶ (A)sigma)}
46. b ∈ {H, (∀ (phi)sigma).𝕀, (psi)p ⊢ _:(T)sigma}
47. b0 ∈ {H, (∀ (phi)sigma) ⊢ _:((T)sigma)[0(𝕀)][psi |⟶ b[0]]}
48. (cT)sigma ∈ H, (∀ (phi)sigma).𝕀 ⊢ Compositon((T)sigma)
49. pres (equiv-fun(f))sigma [psi ⊢→ b] b0
∈ {H, (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))}
50. pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
∈ {H, (∀ (phi)sigma) ⊢ _:((A)sigma)[1(𝕀)][psi |⟶ app((equiv-fun(f))sigma; b)[1]]}
51. pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma)
∈ {H, (∀ (phi)sigma) ⊢ _:((A)sigma)[1(𝕀)][psi |⟶ app((equiv-fun(f))sigma; b)[1]]}
52. H, (∀ (phi)sigma) ⊢ (Path_((A)sigma)[1(𝕀)] pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))
53. w : {H, (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))}
54. pres (equiv-fun(f))sigma [psi ⊢→ b] b0
= w
∈ {H, (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))}
55. (w ∨ <>((app((equiv-fun(f))sigma; b)[1])p))
= w
∈ {H, (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))}
56. ww : {H, (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))}
57. (w ∨ <>((app((equiv-fun(f))sigma; b)[1])p))
= ww
∈ {H, (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))}
58. ww
= w
∈ {H, (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))}
59. equiv-fun(((f)sigma)[1(𝕀)]) ∈ {H ⊢ _:(((T)sigma)[1(𝕀)] ⟶ ((A)sigma)[1(𝕀)])}
60. ww ∈ {H ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); tt'1))}
61. cF : H, ((phi)sigma)[1(𝕀)] ⊢ Compositon(Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1))
62. fiber-comp(H, ((phi)sigma)[1(𝕀)];((T)sigma)[1(𝕀)];((A)sigma)[1(𝕀)];equiv-fun(((f)sigma)[1(𝕀)]);a'1;
(cT)sigma o [1(𝕀)];(cA)sigma o [1(𝕀)])
= cF
∈ H, ((phi)sigma)[1(𝕀)] ⊢ Compositon(Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1))
⊢ ((f)sigma)[1(𝕀)] ∈ {H, ((phi)sigma)[1(𝕀)] ⊢ _:Equiv(((T)sigma)[1(𝕀)];((A)sigma)[1(𝕀)])}
BY
{ SubsumeC ⌜{H ⊢ _:Equiv(((T)sigma)[1(𝕀)];((A)sigma)[1(𝕀)])}⌝⋅ }
1
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. cA : G +⊢ Compositon(A)
4. phi : {G ⊢ _:𝔽}
5. T : {G, phi ⊢ _}
6. cT : composition-function{[i | j]:l, i:l}(G, phi; T)
7. uniform-comp-function{[i | j]:l, i:l}(G, phi; T; cT)
8. f : {G, phi ⊢ _:Equiv(T;A)}
9. H : CubicalSet{j}
10. sigma : H.𝕀 j⟶ G, phi
11. psi : {H ⊢ _:𝔽}
12. b : {H, psi.𝕀 ⊢ _:(T)sigma}
13. b0 : {H ⊢ _:((T)sigma)[0(𝕀)][psi |⟶ (b)[0(𝕀)]]}
14. G ⊢ Glue [phi ⊢→ (T;equiv-fun(f))] A
15. (Glue [phi ⊢→ (T;equiv-fun(f))] A)sigma
= H.𝕀 ⊢ Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma
∈ {H.𝕀 ⊢ _}
16. (T)sigma = H.𝕀 ⊢ Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma ∈ {H.𝕀 ⊢ _}
17. {H.𝕀 ⊢ _:Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma} = {H.𝕀 ⊢ _:(T)sigma} ∈ 𝕌{[i' | j']}
18. {b ∈ {H.𝕀, (psi)p ⊢ _:Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma}}
19. (phi)sigma = 1(𝔽) ∈ {H.𝕀 ⊢ _:𝔽}
20. (equiv-fun(f))sigma ∈ {H.𝕀 ⊢ _:((T ⟶ A))sigma}
21. (equiv-fun(f))sigma ∈ {H.𝕀 ⊢ _:((T)sigma ⟶ (A)sigma)}
22. H ⊢ ((T)sigma)[0(𝕀)]
23. ((equiv-fun(f))sigma)[0(𝕀)] ∈ {H ⊢ _:(((T ⟶ A))sigma)[0(𝕀)]}
24. ((equiv-fun(f))sigma)[0(𝕀)] ∈ {H ⊢ _:(((T)sigma)[0(𝕀)] ⟶ ((A)sigma)[0(𝕀)])}
25. ((phi)sigma)[0(𝕀)] = 1(𝔽) ∈ {H ⊢ _:𝔽}
26. app((equiv-fun(f))sigma; b) ∈ {H.𝕀, (psi)p ⊢ _:(A)sigma}
27. a : {H.𝕀, (psi)p ⊢ _:(A)sigma}
28. unglue(b) = a ∈ {H.𝕀, (psi)p ⊢ _:(A)sigma}
29. a = app((equiv-fun(f))sigma; b) ∈ {H.𝕀, (psi)p ⊢ _:(A)sigma}
30. a0 : {H ⊢ _:((A)sigma)[0(𝕀)]}
31. unglue(b0) = a0 ∈ {H ⊢ _:((A)sigma)[0(𝕀)]}
32. a0 = app(((equiv-fun(f))sigma)[0(𝕀)]; b0) ∈ {H ⊢ _:((A)sigma)[0(𝕀)]}
33. a0 ∈ {H ⊢ _:((A)sigma)[0(𝕀)][psi |⟶ a[0]]}
34. comp (cA)sigma [psi ⊢→ a] a0 ∈ {H ⊢ _:((A)sigma)[1(𝕀)][psi |⟶ a[1]]}
35. a'1 : {H ⊢ _:((A)sigma)[1(𝕀)][psi |⟶ a[1]]}
36. comp (cA)sigma [psi ⊢→ a] a0 = a'1 ∈ {H ⊢ _:((A)sigma)[1(𝕀)][psi |⟶ a[1]]}
37. (H ⊢ ∀ (phi)sigma) = 1(𝔽) ∈ {H ⊢ _:𝔽}
38. xx : {H ⊢ _:((T)sigma)[1(𝕀)]}
39. (cT H sigma psi b b0) = xx ∈ {H ⊢ _:((T)sigma)[1(𝕀)]}
40. t'1 : {H ⊢ _:((T)sigma)[1(𝕀)]}
41. comp (cT)sigma [psi ⊢→ b] b0 = t'1 ∈ {H ⊢ _:((T)sigma)[1(𝕀)]}
42. xx = t'1 ∈ {H ⊢ _:((T)sigma)[1(𝕀)]}
43. tt'1 : {H ⊢ _:((T)sigma)[1(𝕀)]}
44. tt'1 = t'1 ∈ {H ⊢ _:((T)sigma)[1(𝕀)]}
45. (equiv-fun(f))sigma ∈ {H, (∀ (phi)sigma).𝕀 ⊢ _:((T)sigma ⟶ (A)sigma)}
46. b ∈ {H, (∀ (phi)sigma).𝕀, (psi)p ⊢ _:(T)sigma}
47. b0 ∈ {H, (∀ (phi)sigma) ⊢ _:((T)sigma)[0(𝕀)][psi |⟶ b[0]]}
48. (cT)sigma ∈ H, (∀ (phi)sigma).𝕀 ⊢ Compositon((T)sigma)
49. pres (equiv-fun(f))sigma [psi ⊢→ b] b0
∈ {H, (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))}
50. pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
∈ {H, (∀ (phi)sigma) ⊢ _:((A)sigma)[1(𝕀)][psi |⟶ app((equiv-fun(f))sigma; b)[1]]}
51. pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma)
∈ {H, (∀ (phi)sigma) ⊢ _:((A)sigma)[1(𝕀)][psi |⟶ app((equiv-fun(f))sigma; b)[1]]}
52. H, (∀ (phi)sigma) ⊢ (Path_((A)sigma)[1(𝕀)] pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))
53. w : {H, (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))}
54. pres (equiv-fun(f))sigma [psi ⊢→ b] b0
= w
∈ {H, (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))}
55. (w ∨ <>((app((equiv-fun(f))sigma; b)[1])p))
= w
∈ {H, (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))}
56. ww : {H, (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))}
57. (w ∨ <>((app((equiv-fun(f))sigma; b)[1])p))
= ww
∈ {H, (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))}
58. ww
= w
∈ {H, (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))}
59. equiv-fun(((f)sigma)[1(𝕀)]) ∈ {H ⊢ _:(((T)sigma)[1(𝕀)] ⟶ ((A)sigma)[1(𝕀)])}
60. ww ∈ {H ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); tt'1))}
61. cF : H, ((phi)sigma)[1(𝕀)] ⊢ Compositon(Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1))
62. fiber-comp(H, ((phi)sigma)[1(𝕀)];((T)sigma)[1(𝕀)];((A)sigma)[1(𝕀)];equiv-fun(((f)sigma)[1(𝕀)]);a'1;
(cT)sigma o [1(𝕀)];(cA)sigma o [1(𝕀)])
= cF
∈ H, ((phi)sigma)[1(𝕀)] ⊢ Compositon(Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1))
⊢ ((f)sigma)[1(𝕀)] ∈ {H ⊢ _:Equiv(((T)sigma)[1(𝕀)];((A)sigma)[1(𝕀)])}
2
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. cA : G +⊢ Compositon(A)
4. phi : {G ⊢ _:𝔽}
5. T : {G, phi ⊢ _}
6. cT : composition-function{[i | j]:l, i:l}(G, phi; T)
7. uniform-comp-function{[i | j]:l, i:l}(G, phi; T; cT)
8. f : {G, phi ⊢ _:Equiv(T;A)}
9. H : CubicalSet{j}
10. sigma : H.𝕀 j⟶ G, phi
11. psi : {H ⊢ _:𝔽}
12. b : {H, psi.𝕀 ⊢ _:(T)sigma}
13. b0 : {H ⊢ _:((T)sigma)[0(𝕀)][psi |⟶ (b)[0(𝕀)]]}
14. G ⊢ Glue [phi ⊢→ (T;equiv-fun(f))] A
15. (Glue [phi ⊢→ (T;equiv-fun(f))] A)sigma
= H.𝕀 ⊢ Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma
∈ {H.𝕀 ⊢ _}
16. (T)sigma = H.𝕀 ⊢ Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma ∈ {H.𝕀 ⊢ _}
17. {H.𝕀 ⊢ _:Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma} = {H.𝕀 ⊢ _:(T)sigma} ∈ 𝕌{[i' | j']}
18. {b ∈ {H.𝕀, (psi)p ⊢ _:Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma}}
19. (phi)sigma = 1(𝔽) ∈ {H.𝕀 ⊢ _:𝔽}
20. (equiv-fun(f))sigma ∈ {H.𝕀 ⊢ _:((T ⟶ A))sigma}
21. (equiv-fun(f))sigma ∈ {H.𝕀 ⊢ _:((T)sigma ⟶ (A)sigma)}
22. H ⊢ ((T)sigma)[0(𝕀)]
23. ((equiv-fun(f))sigma)[0(𝕀)] ∈ {H ⊢ _:(((T ⟶ A))sigma)[0(𝕀)]}
24. ((equiv-fun(f))sigma)[0(𝕀)] ∈ {H ⊢ _:(((T)sigma)[0(𝕀)] ⟶ ((A)sigma)[0(𝕀)])}
25. ((phi)sigma)[0(𝕀)] = 1(𝔽) ∈ {H ⊢ _:𝔽}
26. app((equiv-fun(f))sigma; b) ∈ {H.𝕀, (psi)p ⊢ _:(A)sigma}
27. a : {H.𝕀, (psi)p ⊢ _:(A)sigma}
28. unglue(b) = a ∈ {H.𝕀, (psi)p ⊢ _:(A)sigma}
29. a = app((equiv-fun(f))sigma; b) ∈ {H.𝕀, (psi)p ⊢ _:(A)sigma}
30. a0 : {H ⊢ _:((A)sigma)[0(𝕀)]}
31. unglue(b0) = a0 ∈ {H ⊢ _:((A)sigma)[0(𝕀)]}
32. a0 = app(((equiv-fun(f))sigma)[0(𝕀)]; b0) ∈ {H ⊢ _:((A)sigma)[0(𝕀)]}
33. a0 ∈ {H ⊢ _:((A)sigma)[0(𝕀)][psi |⟶ a[0]]}
34. comp (cA)sigma [psi ⊢→ a] a0 ∈ {H ⊢ _:((A)sigma)[1(𝕀)][psi |⟶ a[1]]}
35. a'1 : {H ⊢ _:((A)sigma)[1(𝕀)][psi |⟶ a[1]]}
36. comp (cA)sigma [psi ⊢→ a] a0 = a'1 ∈ {H ⊢ _:((A)sigma)[1(𝕀)][psi |⟶ a[1]]}
37. (H ⊢ ∀ (phi)sigma) = 1(𝔽) ∈ {H ⊢ _:𝔽}
38. xx : {H ⊢ _:((T)sigma)[1(𝕀)]}
39. (cT H sigma psi b b0) = xx ∈ {H ⊢ _:((T)sigma)[1(𝕀)]}
40. t'1 : {H ⊢ _:((T)sigma)[1(𝕀)]}
41. comp (cT)sigma [psi ⊢→ b] b0 = t'1 ∈ {H ⊢ _:((T)sigma)[1(𝕀)]}
42. xx = t'1 ∈ {H ⊢ _:((T)sigma)[1(𝕀)]}
43. tt'1 : {H ⊢ _:((T)sigma)[1(𝕀)]}
44. tt'1 = t'1 ∈ {H ⊢ _:((T)sigma)[1(𝕀)]}
45. (equiv-fun(f))sigma ∈ {H, (∀ (phi)sigma).𝕀 ⊢ _:((T)sigma ⟶ (A)sigma)}
46. b ∈ {H, (∀ (phi)sigma).𝕀, (psi)p ⊢ _:(T)sigma}
47. b0 ∈ {H, (∀ (phi)sigma) ⊢ _:((T)sigma)[0(𝕀)][psi |⟶ b[0]]}
48. (cT)sigma ∈ H, (∀ (phi)sigma).𝕀 ⊢ Compositon((T)sigma)
49. pres (equiv-fun(f))sigma [psi ⊢→ b] b0
∈ {H, (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))}
50. pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
∈ {H, (∀ (phi)sigma) ⊢ _:((A)sigma)[1(𝕀)][psi |⟶ app((equiv-fun(f))sigma; b)[1]]}
51. pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma)
∈ {H, (∀ (phi)sigma) ⊢ _:((A)sigma)[1(𝕀)][psi |⟶ app((equiv-fun(f))sigma; b)[1]]}
52. H, (∀ (phi)sigma) ⊢ (Path_((A)sigma)[1(𝕀)] pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))
53. w : {H, (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))}
54. pres (equiv-fun(f))sigma [psi ⊢→ b] b0
= w
∈ {H, (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))}
55. (w ∨ <>((app((equiv-fun(f))sigma; b)[1])p))
= w
∈ {H, (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))}
56. ww : {H, (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))}
57. (w ∨ <>((app((equiv-fun(f))sigma; b)[1])p))
= ww
∈ {H, (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))}
58. ww
= w
∈ {H, (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))}
59. equiv-fun(((f)sigma)[1(𝕀)]) ∈ {H ⊢ _:(((T)sigma)[1(𝕀)] ⟶ ((A)sigma)[1(𝕀)])}
60. ww ∈ {H ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); tt'1))}
61. cF : H, ((phi)sigma)[1(𝕀)] ⊢ Compositon(Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1))
62. fiber-comp(H, ((phi)sigma)[1(𝕀)];((T)sigma)[1(𝕀)];((A)sigma)[1(𝕀)];equiv-fun(((f)sigma)[1(𝕀)]);a'1;
(cT)sigma o [1(𝕀)];(cA)sigma o [1(𝕀)])
= cF
∈ H, ((phi)sigma)[1(𝕀)] ⊢ Compositon(Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1))
63. ((f)sigma)[1(𝕀)] = ((f)sigma)[1(𝕀)] ∈ {H ⊢ _:Equiv(((T)sigma)[1(𝕀)];((A)sigma)[1(𝕀)])}
⊢ {H ⊢ _:Equiv(((T)sigma)[1(𝕀)];((A)sigma)[1(𝕀)])}
⊆r {H, ((phi)sigma)[1(𝕀)] ⊢ _:Equiv(((T)sigma)[1(𝕀)];((A)sigma)[1(𝕀)])}
Latex:
Latex:
.....assertion.....
1. G : CubicalSet\{j\}
2. A : \{G \mvdash{} \_\}
3. cA : G +\mvdash{} Compositon(A)
4. phi : \{G \mvdash{} \_:\mBbbF{}\}
5. T : \{G, phi \mvdash{} \_\}
6. cT : composition-function\{[i | j]:l, i:l\}(G, phi; T)
7. uniform-comp-function\{[i | j]:l, i:l\}(G, phi; T; cT)
8. f : \{G, phi \mvdash{} \_:Equiv(T;A)\}
9. H : CubicalSet\{j\}
10. sigma : H.\mBbbI{} j{}\mrightarrow{} G, phi
11. psi : \{H \mvdash{} \_:\mBbbF{}\}
12. b : \{H, psi.\mBbbI{} \mvdash{} \_:(T)sigma\}
13. b0 : \{H \mvdash{} \_:((T)sigma)[0(\mBbbI{})][psi |{}\mrightarrow{} (b)[0(\mBbbI{})]]\}
14. G \mvdash{} Glue [phi \mvdash{}\mrightarrow{} (T;equiv-fun(f))] A
15. (Glue [phi \mvdash{}\mrightarrow{} (T;equiv-fun(f))] A)sigma
= H.\mBbbI{} \mvdash{} Glue [(phi)sigma \mvdash{}\mrightarrow{} ((T)sigma;(equiv-fun(f))sigma)] (A)sigma
16. (T)sigma = H.\mBbbI{} \mvdash{} Glue [(phi)sigma \mvdash{}\mrightarrow{} ((T)sigma;(equiv-fun(f))sigma)] (A)sigma
17. \{H.\mBbbI{} \mvdash{} \_:Glue [(phi)sigma \mvdash{}\mrightarrow{} ((T)sigma;(equiv-fun(f))sigma)] (A)sigma\} = \{H.\mBbbI{} \mvdash{} \_:(T)sigma\}
18. \{b \mmember{} \{H.\mBbbI{}, (psi)p \mvdash{} \_:Glue [(phi)sigma \mvdash{}\mrightarrow{} ((T)sigma;(equiv-fun(f))sigma)] (A)sigma\}\}
19. (phi)sigma = 1(\mBbbF{})
20. (equiv-fun(f))sigma \mmember{} \{H.\mBbbI{} \mvdash{} \_:((T {}\mrightarrow{} A))sigma\}
21. (equiv-fun(f))sigma \mmember{} \{H.\mBbbI{} \mvdash{} \_:((T)sigma {}\mrightarrow{} (A)sigma)\}
22. H \mvdash{} ((T)sigma)[0(\mBbbI{})]
23. ((equiv-fun(f))sigma)[0(\mBbbI{})] \mmember{} \{H \mvdash{} \_:(((T {}\mrightarrow{} A))sigma)[0(\mBbbI{})]\}
24. ((equiv-fun(f))sigma)[0(\mBbbI{})] \mmember{} \{H \mvdash{} \_:(((T)sigma)[0(\mBbbI{})] {}\mrightarrow{} ((A)sigma)[0(\mBbbI{})])\}
25. ((phi)sigma)[0(\mBbbI{})] = 1(\mBbbF{})
26. app((equiv-fun(f))sigma; b) \mmember{} \{H.\mBbbI{}, (psi)p \mvdash{} \_:(A)sigma\}
27. a : \{H.\mBbbI{}, (psi)p \mvdash{} \_:(A)sigma\}
28. unglue(b) = a
29. a = app((equiv-fun(f))sigma; b)
30. a0 : \{H \mvdash{} \_:((A)sigma)[0(\mBbbI{})]\}
31. unglue(b0) = a0
32. a0 = app(((equiv-fun(f))sigma)[0(\mBbbI{})]; b0)
33. a0 \mmember{} \{H \mvdash{} \_:((A)sigma)[0(\mBbbI{})][psi |{}\mrightarrow{} a[0]]\}
34. comp (cA)sigma [psi \mvdash{}\mrightarrow{} a] a0 \mmember{} \{H \mvdash{} \_:((A)sigma)[1(\mBbbI{})][psi |{}\mrightarrow{} a[1]]\}
35. a'1 : \{H \mvdash{} \_:((A)sigma)[1(\mBbbI{})][psi |{}\mrightarrow{} a[1]]\}
36. comp (cA)sigma [psi \mvdash{}\mrightarrow{} a] a0 = a'1
37. (H \mvdash{} \mforall{} (phi)sigma) = 1(\mBbbF{})
38. xx : \{H \mvdash{} \_:((T)sigma)[1(\mBbbI{})]\}
39. (cT H sigma psi b b0) = xx
40. t'1 : \{H \mvdash{} \_:((T)sigma)[1(\mBbbI{})]\}
41. comp (cT)sigma [psi \mvdash{}\mrightarrow{} b] b0 = t'1
42. xx = t'1
43. tt'1 : \{H \mvdash{} \_:((T)sigma)[1(\mBbbI{})]\}
44. tt'1 = t'1
45. (equiv-fun(f))sigma \mmember{} \{H, (\mforall{} (phi)sigma).\mBbbI{} \mvdash{} \_:((T)sigma {}\mrightarrow{} (A)sigma)\}
46. b \mmember{} \{H, (\mforall{} (phi)sigma).\mBbbI{}, (psi)p \mvdash{} \_:(T)sigma\}
47. b0 \mmember{} \{H, (\mforall{} (phi)sigma) \mvdash{} \_:((T)sigma)[0(\mBbbI{})][psi |{}\mrightarrow{} b[0]]\}
48. (cT)sigma \mmember{} H, (\mforall{} (phi)sigma).\mBbbI{} \mvdash{} Compositon((T)sigma)
49. pres (equiv-fun(f))sigma [psi \mvdash{}\mrightarrow{} b] b0
\mmember{} \{H, (\mforall{} (phi)sigma) \mvdash{} \_:(Path\_((A)sigma)[1(\mBbbI{})] pres-c1(H, (\mforall{} (phi)sigma);psi;
(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (\mforall{} (phi)sigma);psi;(equiv-fun(f))sigma;b;
b0;(cT)sigma))\}
50. pres-c1(H, (\mforall{} (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
\mmember{} \{H, (\mforall{} (phi)sigma) \mvdash{} \_:((A)sigma)[1(\mBbbI{})][psi |{}\mrightarrow{} app((equiv-fun(f))sigma; b)[1]]\}
51. pres-c2(H, (\mforall{} (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma)
\mmember{} \{H, (\mforall{} (phi)sigma) \mvdash{} \_:((A)sigma)[1(\mBbbI{})][psi |{}\mrightarrow{} app((equiv-fun(f))sigma; b)[1]]\}
52. H, (\mforall{} (phi)sigma) \mvdash{} (Path\_((A)sigma)[1(\mBbbI{})] pres-c1(H, (\mforall{} (phi)sigma);psi;(equiv-fun(f))sigma;b;
b0;(cA)sigma)
pres-c2(H, (\mforall{} (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))
53. w : \{H, (\mforall{} (phi)sigma) \mvdash{} \_:(Path\_((A)sigma)[1(\mBbbI{})] pres-c1(H, (\mforall{} (phi)sigma);psi;
(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (\mforall{} (phi)sigma);psi;(equiv-fun(f))sigma;b;
b0;(cT)sigma))\}
54. pres (equiv-fun(f))sigma [psi \mvdash{}\mrightarrow{} b] b0 = w
55. (w \mvee{} <>((app((equiv-fun(f))sigma; b)[1])p)) = w
56. ww : \{H, (\mforall{} (phi)sigma) \mvdash{} \_:(Path\_((A)sigma)[1(\mBbbI{})] pres-c1(H, (\mforall{} (phi)sigma);psi;
(equiv-fun(f))sigma;b;b0;(cA)sigma)
pres-c2(H, (\mforall{} (phi)sigma);psi;(equiv-fun(f))sigma;b;
b0;(cT)sigma))\}
57. (w \mvee{} <>((app((equiv-fun(f))sigma; b)[1])p)) = ww
58. ww = w
59. equiv-fun(((f)sigma)[1(\mBbbI{})]) \mmember{} \{H \mvdash{} \_:(((T)sigma)[1(\mBbbI{})] {}\mrightarrow{} ((A)sigma)[1(\mBbbI{})])\}
60. ww \mmember{} \{H \mvdash{} \_:(Path\_((A)sigma)[1(\mBbbI{})] a'1 app(equiv-fun(((f)sigma)[1(\mBbbI{})]); tt'1))\}
61. cF : H, ((phi)sigma)[1(\mBbbI{})] \mvdash{} Compositon(Fiber(equiv-fun(((f)sigma)[1(\mBbbI{})]);a'1))
62. fiber-comp(H, ((phi)sigma)[1(\mBbbI{})];((T)sigma)[1(\mBbbI{})];((A)sigma)[1(\mBbbI{})];equiv-fun(((f)sigma)[1(\mBbbI{})]);
a'1;(cT)sigma o [1(\mBbbI{})];(cA)sigma o [1(\mBbbI{})])
= cF
\mvdash{} ((f)sigma)[1(\mBbbI{})] \mmember{} \{H, ((phi)sigma)[1(\mBbbI{})] \mvdash{} \_:Equiv(((T)sigma)[1(\mBbbI{})];((A)sigma)[1(\mBbbI{})])\}
By
Latex:
SubsumeC \mkleeneopen{}\{H \mvdash{} \_:Equiv(((T)sigma)[1(\mBbbI{})];((A)sigma)[1(\mBbbI{})])\}\mkleeneclose{}\mcdot{}
Home
Index