Step
*
2
1
1
1
2
1
1
1
of Lemma
path_comp_wf
.....equality.....
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. a : {G ⊢ _:A}
4. b : {G ⊢ _:A}
5. cA : G ⊢ Compositon(A)
6. path_comp(G;A;a;b;
cA) ∈ composition-function{j:l,i:l}(G;(Path_A a b))
7. H : CubicalSet{j}
8. K : CubicalSet{j}
9. tau : K j⟶ H
10. sigma : H.𝕀 j⟶ G
11. phi : {H ⊢ _:𝔽}
12. u : {H, phi.𝕀 ⊢ _:((Path_A a b))sigma}
13. a0 : {H ⊢ _:(((Path_A a b))sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
14. {H, phi.𝕀 ⊢ _:((Path_A a b))sigma} = {H, phi.𝕀 ⊢ _:(Path_(A)sigma (a)sigma (b)sigma)} ∈ 𝕌{[i' | j']}
15. a0 ∈ {H ⊢ _:(Path_((A)sigma)[0(𝕀)] ((a)sigma)[0(𝕀)] ((b)sigma)[0(𝕀)])}
16. a0 @ 0(𝕀) ∈ {H ⊢ _:((A)sigma)[0(𝕀)]}
17. p+ ∈ H.𝕀.𝕀 ij⟶ H.𝕀
18. ∀[u:{H.𝕀, ((phi)p ∨ ((q=0) ∨ (q=1))).𝕀 ⊢ _:((A)sigma)p+}].
∀[a0:{H.𝕀 ⊢ _:(((A)sigma)p+)[0(𝕀)][((phi)p ∨ ((q=0) ∨ (q=1))) |⟶ (u)[0(𝕀)]]}].
(comp ((cA)sigma)p+ [((phi)p ∨ ((q=0) ∨ (q=1))) ⊢→ u] a0
∈ {H.𝕀 ⊢ _:(((A)sigma)[1(𝕀)])p[((phi)p ∨ ((q=0) ∨ (q=1))) |⟶ (u)[1(𝕀)]]})
19. (u)p+ ∈ {H.𝕀.𝕀, ((phi)p)p ⊢ _:(((Path_A a b))sigma)p+}
20. (u)p+ ∈ {H.𝕀, (phi)p.𝕀 ⊢ _:(((Path_A a b))sigma)p+}
21. {H.𝕀.𝕀 ⊢ _:((A)sigma)p+} ⊆r {H.𝕀, (phi)p.𝕀 ⊢ _:((A)sigma)p+}
22. {H.𝕀.𝕀 ⊢ _:((A)sigma)p+} ⊆r {H.𝕀, (phi)p.𝕀 ⊢ _:((A)sigma)p+}
23. ((b)sigma)p+ ∈ {H.𝕀.𝕀 ⊢ _:((A)sigma)p+}
24. ((a)sigma)p+ ∈ {H.𝕀.𝕀 ⊢ _:((A)sigma)p+}
25. (u)p+ ∈ {H.𝕀, (phi)p.𝕀 ⊢ _:(Path_((A)sigma)p+ ((a)sigma)p+ ((b)sigma)p+)}
26. path_term((phi)p; (u)p+; ((a)sigma)p+; ((b)sigma)p+; q) ∈ {H.𝕀, ((phi)p ∨ ((q=0) ∨ (q=1))).𝕀 ⊢ _:((A)sigma)p+}
27. (a0)p @ q ∈ {H.𝕀 ⊢ _:(((A)sigma)p+)[0(𝕀)][((phi)p ∨ ((q=0) ∨ (q=1))) |⟶ (path_term((phi)p;
(u)p+;
((a)sigma)p+;
((b)sigma)p+;
q))[0(𝕀)]]}
28. ((((Path_A a b))sigma)[1(𝕀)])p
= (H.𝕀 ⊢ Path_(((A)sigma)[1(𝕀)])p (((a)sigma)[1(𝕀)])p (((b)sigma)[1(𝕀)])p)
∈ {H.𝕀 ⊢ _}
29. {H.𝕀 ⊢ _:(((A)sigma)[1(𝕀)])p[((phi)p ∨ ((q=0) ∨ (q=1)))
|⟶ path-term((phi)p;((u)[1(𝕀)])p;(((a)sigma)[1(𝕀)])p;(((b)sigma)[1(𝕀)])p;q)]} ∈ 𝕌{[i' | j']}
30. (comp ((cA)sigma)p+ [((phi)p ∨ ((q=0) ∨ (q=1))) ⊢→ path_term((phi)p; (u)p+; ((a)sigma)p+; ((b)sigma)p+; q)]
(a0)p @ q)tau+
= comp (((cA)sigma)p+)tau++ [(((phi)p ∨ ((q=0) ∨ (q=1))))tau+ ⊢→ (path_term((phi)p; (u)p+; ((a)sigma)p+; ((b)sigma)p+; q
))tau++] ((a0)p @ q)tau+
∈ {K.𝕀 ⊢ _:((((A)sigma)p+)tau++)[1(𝕀)][(((phi)p ∨ ((q=0) ∨ (q=1))))tau+ |⟶ ((path_term((phi)p;
(u)p+;
((a)sigma)p+;
((b)sigma)p+;
q))tau++)[1(𝕀)]]}
⊢ comp ((cA)sigma o tau+)p+ [(((phi)tau)p ∨ ((q=0) ∨ (q=1))) ⊢→ path_term(((phi)tau)p;
((u)tau+)p+;
((a)sigma o tau+)p+;
((b)sigma o tau+)p+;
q)] ((a0)tau)p @ q
~ comp (((cA)sigma)p+)tau++ [(((phi)p ∨ ((q=0) ∨ (q=1))))tau+ ⊢→ (path_term((phi)p; (u)p+; ((a)sigma)p+; ((b)sigma)p+; q
))tau++] ((a0)p @ q)tau+
BY
{ (EqCD THEN Try (Trivial)) }
1
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. a : {G ⊢ _:A}
4. b : {G ⊢ _:A}
5. cA : G ⊢ Compositon(A)
6. path_comp(G;A;a;b;
cA) ∈ composition-function{j:l,i:l}(G;(Path_A a b))
7. H : CubicalSet{j}
8. K : CubicalSet{j}
9. tau : K j⟶ H
10. sigma : H.𝕀 j⟶ G
11. phi : {H ⊢ _:𝔽}
12. u : {H, phi.𝕀 ⊢ _:((Path_A a b))sigma}
13. a0 : {H ⊢ _:(((Path_A a b))sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
14. {H, phi.𝕀 ⊢ _:((Path_A a b))sigma} = {H, phi.𝕀 ⊢ _:(Path_(A)sigma (a)sigma (b)sigma)} ∈ 𝕌{[i' | j']}
15. a0 ∈ {H ⊢ _:(Path_((A)sigma)[0(𝕀)] ((a)sigma)[0(𝕀)] ((b)sigma)[0(𝕀)])}
16. a0 @ 0(𝕀) ∈ {H ⊢ _:((A)sigma)[0(𝕀)]}
17. p+ ∈ H.𝕀.𝕀 ij⟶ H.𝕀
18. ∀[u:{H.𝕀, ((phi)p ∨ ((q=0) ∨ (q=1))).𝕀 ⊢ _:((A)sigma)p+}].
∀[a0:{H.𝕀 ⊢ _:(((A)sigma)p+)[0(𝕀)][((phi)p ∨ ((q=0) ∨ (q=1))) |⟶ (u)[0(𝕀)]]}].
(comp ((cA)sigma)p+ [((phi)p ∨ ((q=0) ∨ (q=1))) ⊢→ u] a0
∈ {H.𝕀 ⊢ _:(((A)sigma)[1(𝕀)])p[((phi)p ∨ ((q=0) ∨ (q=1))) |⟶ (u)[1(𝕀)]]})
19. (u)p+ ∈ {H.𝕀.𝕀, ((phi)p)p ⊢ _:(((Path_A a b))sigma)p+}
20. (u)p+ ∈ {H.𝕀, (phi)p.𝕀 ⊢ _:(((Path_A a b))sigma)p+}
21. {H.𝕀.𝕀 ⊢ _:((A)sigma)p+} ⊆r {H.𝕀, (phi)p.𝕀 ⊢ _:((A)sigma)p+}
22. {H.𝕀.𝕀 ⊢ _:((A)sigma)p+} ⊆r {H.𝕀, (phi)p.𝕀 ⊢ _:((A)sigma)p+}
23. ((b)sigma)p+ ∈ {H.𝕀.𝕀 ⊢ _:((A)sigma)p+}
24. ((a)sigma)p+ ∈ {H.𝕀.𝕀 ⊢ _:((A)sigma)p+}
25. (u)p+ ∈ {H.𝕀, (phi)p.𝕀 ⊢ _:(Path_((A)sigma)p+ ((a)sigma)p+ ((b)sigma)p+)}
26. path_term((phi)p; (u)p+; ((a)sigma)p+; ((b)sigma)p+; q) ∈ {H.𝕀, ((phi)p ∨ ((q=0) ∨ (q=1))).𝕀 ⊢ _:((A)sigma)p+}
27. (a0)p @ q ∈ {H.𝕀 ⊢ _:(((A)sigma)p+)[0(𝕀)][((phi)p ∨ ((q=0) ∨ (q=1))) |⟶ (path_term((phi)p;
(u)p+;
((a)sigma)p+;
((b)sigma)p+;
q))[0(𝕀)]]}
28. ((((Path_A a b))sigma)[1(𝕀)])p
= (H.𝕀 ⊢ Path_(((A)sigma)[1(𝕀)])p (((a)sigma)[1(𝕀)])p (((b)sigma)[1(𝕀)])p)
∈ {H.𝕀 ⊢ _}
29. {H.𝕀 ⊢ _:(((A)sigma)[1(𝕀)])p[((phi)p ∨ ((q=0) ∨ (q=1)))
|⟶ path-term((phi)p;((u)[1(𝕀)])p;(((a)sigma)[1(𝕀)])p;(((b)sigma)[1(𝕀)])p;q)]} ∈ 𝕌{[i' | j']}
30. (comp ((cA)sigma)p+ [((phi)p ∨ ((q=0) ∨ (q=1))) ⊢→ path_term((phi)p; (u)p+; ((a)sigma)p+; ((b)sigma)p+; q)]
(a0)p @ q)tau+
= comp (((cA)sigma)p+)tau++ [(((phi)p ∨ ((q=0) ∨ (q=1))))tau+ ⊢→ (path_term((phi)p; (u)p+; ((a)sigma)p+; ((b)sigma)p+; q
))tau++] ((a0)p @ q)tau+
∈ {K.𝕀 ⊢ _:((((A)sigma)p+)tau++)[1(𝕀)][(((phi)p ∨ ((q=0) ∨ (q=1))))tau+ |⟶ ((path_term((phi)p;
(u)p+;
((a)sigma)p+;
((b)sigma)p+;
q))tau++)[1(𝕀)]]}
⊢ ((cA)sigma o tau+)p+ ~ (((cA)sigma)p+)tau++
2
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. a : {G ⊢ _:A}
4. b : {G ⊢ _:A}
5. cA : G ⊢ Compositon(A)
6. path_comp(G;A;a;b;
cA) ∈ composition-function{j:l,i:l}(G;(Path_A a b))
7. H : CubicalSet{j}
8. K : CubicalSet{j}
9. tau : K j⟶ H
10. sigma : H.𝕀 j⟶ G
11. phi : {H ⊢ _:𝔽}
12. u : {H, phi.𝕀 ⊢ _:((Path_A a b))sigma}
13. a0 : {H ⊢ _:(((Path_A a b))sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
14. {H, phi.𝕀 ⊢ _:((Path_A a b))sigma} = {H, phi.𝕀 ⊢ _:(Path_(A)sigma (a)sigma (b)sigma)} ∈ 𝕌{[i' | j']}
15. a0 ∈ {H ⊢ _:(Path_((A)sigma)[0(𝕀)] ((a)sigma)[0(𝕀)] ((b)sigma)[0(𝕀)])}
16. a0 @ 0(𝕀) ∈ {H ⊢ _:((A)sigma)[0(𝕀)]}
17. p+ ∈ H.𝕀.𝕀 ij⟶ H.𝕀
18. ∀[u:{H.𝕀, ((phi)p ∨ ((q=0) ∨ (q=1))).𝕀 ⊢ _:((A)sigma)p+}].
∀[a0:{H.𝕀 ⊢ _:(((A)sigma)p+)[0(𝕀)][((phi)p ∨ ((q=0) ∨ (q=1))) |⟶ (u)[0(𝕀)]]}].
(comp ((cA)sigma)p+ [((phi)p ∨ ((q=0) ∨ (q=1))) ⊢→ u] a0
∈ {H.𝕀 ⊢ _:(((A)sigma)[1(𝕀)])p[((phi)p ∨ ((q=0) ∨ (q=1))) |⟶ (u)[1(𝕀)]]})
19. (u)p+ ∈ {H.𝕀.𝕀, ((phi)p)p ⊢ _:(((Path_A a b))sigma)p+}
20. (u)p+ ∈ {H.𝕀, (phi)p.𝕀 ⊢ _:(((Path_A a b))sigma)p+}
21. {H.𝕀.𝕀 ⊢ _:((A)sigma)p+} ⊆r {H.𝕀, (phi)p.𝕀 ⊢ _:((A)sigma)p+}
22. {H.𝕀.𝕀 ⊢ _:((A)sigma)p+} ⊆r {H.𝕀, (phi)p.𝕀 ⊢ _:((A)sigma)p+}
23. ((b)sigma)p+ ∈ {H.𝕀.𝕀 ⊢ _:((A)sigma)p+}
24. ((a)sigma)p+ ∈ {H.𝕀.𝕀 ⊢ _:((A)sigma)p+}
25. (u)p+ ∈ {H.𝕀, (phi)p.𝕀 ⊢ _:(Path_((A)sigma)p+ ((a)sigma)p+ ((b)sigma)p+)}
26. path_term((phi)p; (u)p+; ((a)sigma)p+; ((b)sigma)p+; q) ∈ {H.𝕀, ((phi)p ∨ ((q=0) ∨ (q=1))).𝕀 ⊢ _:((A)sigma)p+}
27. (a0)p @ q ∈ {H.𝕀 ⊢ _:(((A)sigma)p+)[0(𝕀)][((phi)p ∨ ((q=0) ∨ (q=1))) |⟶ (path_term((phi)p;
(u)p+;
((a)sigma)p+;
((b)sigma)p+;
q))[0(𝕀)]]}
28. ((((Path_A a b))sigma)[1(𝕀)])p
= (H.𝕀 ⊢ Path_(((A)sigma)[1(𝕀)])p (((a)sigma)[1(𝕀)])p (((b)sigma)[1(𝕀)])p)
∈ {H.𝕀 ⊢ _}
29. {H.𝕀 ⊢ _:(((A)sigma)[1(𝕀)])p[((phi)p ∨ ((q=0) ∨ (q=1)))
|⟶ path-term((phi)p;((u)[1(𝕀)])p;(((a)sigma)[1(𝕀)])p;(((b)sigma)[1(𝕀)])p;q)]} ∈ 𝕌{[i' | j']}
30. (comp ((cA)sigma)p+ [((phi)p ∨ ((q=0) ∨ (q=1))) ⊢→ path_term((phi)p; (u)p+; ((a)sigma)p+; ((b)sigma)p+; q)]
(a0)p @ q)tau+
= comp (((cA)sigma)p+)tau++ [(((phi)p ∨ ((q=0) ∨ (q=1))))tau+ ⊢→ (path_term((phi)p; (u)p+; ((a)sigma)p+; ((b)sigma)p+; q
))tau++] ((a0)p @ q)tau+
∈ {K.𝕀 ⊢ _:((((A)sigma)p+)tau++)[1(𝕀)][(((phi)p ∨ ((q=0) ∨ (q=1))))tau+ |⟶ ((path_term((phi)p;
(u)p+;
((a)sigma)p+;
((b)sigma)p+;
q))tau++)[1(𝕀)]]}
⊢ (((phi)tau)p ∨ ((q=0) ∨ (q=1))) ~ (((phi)p ∨ ((q=0) ∨ (q=1))))tau+
3
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. a : {G ⊢ _:A}
4. b : {G ⊢ _:A}
5. cA : G ⊢ Compositon(A)
6. path_comp(G;A;a;b;
cA) ∈ composition-function{j:l,i:l}(G;(Path_A a b))
7. H : CubicalSet{j}
8. K : CubicalSet{j}
9. tau : K j⟶ H
10. sigma : H.𝕀 j⟶ G
11. phi : {H ⊢ _:𝔽}
12. u : {H, phi.𝕀 ⊢ _:((Path_A a b))sigma}
13. a0 : {H ⊢ _:(((Path_A a b))sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
14. {H, phi.𝕀 ⊢ _:((Path_A a b))sigma} = {H, phi.𝕀 ⊢ _:(Path_(A)sigma (a)sigma (b)sigma)} ∈ 𝕌{[i' | j']}
15. a0 ∈ {H ⊢ _:(Path_((A)sigma)[0(𝕀)] ((a)sigma)[0(𝕀)] ((b)sigma)[0(𝕀)])}
16. a0 @ 0(𝕀) ∈ {H ⊢ _:((A)sigma)[0(𝕀)]}
17. p+ ∈ H.𝕀.𝕀 ij⟶ H.𝕀
18. ∀[u:{H.𝕀, ((phi)p ∨ ((q=0) ∨ (q=1))).𝕀 ⊢ _:((A)sigma)p+}].
∀[a0:{H.𝕀 ⊢ _:(((A)sigma)p+)[0(𝕀)][((phi)p ∨ ((q=0) ∨ (q=1))) |⟶ (u)[0(𝕀)]]}].
(comp ((cA)sigma)p+ [((phi)p ∨ ((q=0) ∨ (q=1))) ⊢→ u] a0
∈ {H.𝕀 ⊢ _:(((A)sigma)[1(𝕀)])p[((phi)p ∨ ((q=0) ∨ (q=1))) |⟶ (u)[1(𝕀)]]})
19. (u)p+ ∈ {H.𝕀.𝕀, ((phi)p)p ⊢ _:(((Path_A a b))sigma)p+}
20. (u)p+ ∈ {H.𝕀, (phi)p.𝕀 ⊢ _:(((Path_A a b))sigma)p+}
21. {H.𝕀.𝕀 ⊢ _:((A)sigma)p+} ⊆r {H.𝕀, (phi)p.𝕀 ⊢ _:((A)sigma)p+}
22. {H.𝕀.𝕀 ⊢ _:((A)sigma)p+} ⊆r {H.𝕀, (phi)p.𝕀 ⊢ _:((A)sigma)p+}
23. ((b)sigma)p+ ∈ {H.𝕀.𝕀 ⊢ _:((A)sigma)p+}
24. ((a)sigma)p+ ∈ {H.𝕀.𝕀 ⊢ _:((A)sigma)p+}
25. (u)p+ ∈ {H.𝕀, (phi)p.𝕀 ⊢ _:(Path_((A)sigma)p+ ((a)sigma)p+ ((b)sigma)p+)}
26. path_term((phi)p; (u)p+; ((a)sigma)p+; ((b)sigma)p+; q) ∈ {H.𝕀, ((phi)p ∨ ((q=0) ∨ (q=1))).𝕀 ⊢ _:((A)sigma)p+}
27. (a0)p @ q ∈ {H.𝕀 ⊢ _:(((A)sigma)p+)[0(𝕀)][((phi)p ∨ ((q=0) ∨ (q=1))) |⟶ (path_term((phi)p;
(u)p+;
((a)sigma)p+;
((b)sigma)p+;
q))[0(𝕀)]]}
28. ((((Path_A a b))sigma)[1(𝕀)])p
= (H.𝕀 ⊢ Path_(((A)sigma)[1(𝕀)])p (((a)sigma)[1(𝕀)])p (((b)sigma)[1(𝕀)])p)
∈ {H.𝕀 ⊢ _}
29. {H.𝕀 ⊢ _:(((A)sigma)[1(𝕀)])p[((phi)p ∨ ((q=0) ∨ (q=1)))
|⟶ path-term((phi)p;((u)[1(𝕀)])p;(((a)sigma)[1(𝕀)])p;(((b)sigma)[1(𝕀)])p;q)]} ∈ 𝕌{[i' | j']}
30. (comp ((cA)sigma)p+ [((phi)p ∨ ((q=0) ∨ (q=1))) ⊢→ path_term((phi)p; (u)p+; ((a)sigma)p+; ((b)sigma)p+; q)]
(a0)p @ q)tau+
= comp (((cA)sigma)p+)tau++ [(((phi)p ∨ ((q=0) ∨ (q=1))))tau+ ⊢→ (path_term((phi)p; (u)p+; ((a)sigma)p+; ((b)sigma)p+; q
))tau++] ((a0)p @ q)tau+
∈ {K.𝕀 ⊢ _:((((A)sigma)p+)tau++)[1(𝕀)][(((phi)p ∨ ((q=0) ∨ (q=1))))tau+ |⟶ ((path_term((phi)p;
(u)p+;
((a)sigma)p+;
((b)sigma)p+;
q))tau++)[1(𝕀)]]}
⊢ path_term(((phi)tau)p; ((u)tau+)p+; ((a)sigma o tau+)p+; ((b)sigma o tau+)p+; q) ~ (path_term((phi)p;
(u)p+;
((a)sigma)p+;
((b)sigma)p+;
q))tau++
4
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. a : {G ⊢ _:A}
4. b : {G ⊢ _:A}
5. cA : G ⊢ Compositon(A)
6. path_comp(G;A;a;b;
cA) ∈ composition-function{j:l,i:l}(G;(Path_A a b))
7. H : CubicalSet{j}
8. K : CubicalSet{j}
9. tau : K j⟶ H
10. sigma : H.𝕀 j⟶ G
11. phi : {H ⊢ _:𝔽}
12. u : {H, phi.𝕀 ⊢ _:((Path_A a b))sigma}
13. a0 : {H ⊢ _:(((Path_A a b))sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
14. {H, phi.𝕀 ⊢ _:((Path_A a b))sigma} = {H, phi.𝕀 ⊢ _:(Path_(A)sigma (a)sigma (b)sigma)} ∈ 𝕌{[i' | j']}
15. a0 ∈ {H ⊢ _:(Path_((A)sigma)[0(𝕀)] ((a)sigma)[0(𝕀)] ((b)sigma)[0(𝕀)])}
16. a0 @ 0(𝕀) ∈ {H ⊢ _:((A)sigma)[0(𝕀)]}
17. p+ ∈ H.𝕀.𝕀 ij⟶ H.𝕀
18. ∀[u:{H.𝕀, ((phi)p ∨ ((q=0) ∨ (q=1))).𝕀 ⊢ _:((A)sigma)p+}].
∀[a0:{H.𝕀 ⊢ _:(((A)sigma)p+)[0(𝕀)][((phi)p ∨ ((q=0) ∨ (q=1))) |⟶ (u)[0(𝕀)]]}].
(comp ((cA)sigma)p+ [((phi)p ∨ ((q=0) ∨ (q=1))) ⊢→ u] a0
∈ {H.𝕀 ⊢ _:(((A)sigma)[1(𝕀)])p[((phi)p ∨ ((q=0) ∨ (q=1))) |⟶ (u)[1(𝕀)]]})
19. (u)p+ ∈ {H.𝕀.𝕀, ((phi)p)p ⊢ _:(((Path_A a b))sigma)p+}
20. (u)p+ ∈ {H.𝕀, (phi)p.𝕀 ⊢ _:(((Path_A a b))sigma)p+}
21. {H.𝕀.𝕀 ⊢ _:((A)sigma)p+} ⊆r {H.𝕀, (phi)p.𝕀 ⊢ _:((A)sigma)p+}
22. {H.𝕀.𝕀 ⊢ _:((A)sigma)p+} ⊆r {H.𝕀, (phi)p.𝕀 ⊢ _:((A)sigma)p+}
23. ((b)sigma)p+ ∈ {H.𝕀.𝕀 ⊢ _:((A)sigma)p+}
24. ((a)sigma)p+ ∈ {H.𝕀.𝕀 ⊢ _:((A)sigma)p+}
25. (u)p+ ∈ {H.𝕀, (phi)p.𝕀 ⊢ _:(Path_((A)sigma)p+ ((a)sigma)p+ ((b)sigma)p+)}
26. path_term((phi)p; (u)p+; ((a)sigma)p+; ((b)sigma)p+; q) ∈ {H.𝕀, ((phi)p ∨ ((q=0) ∨ (q=1))).𝕀 ⊢ _:((A)sigma)p+}
27. (a0)p @ q ∈ {H.𝕀 ⊢ _:(((A)sigma)p+)[0(𝕀)][((phi)p ∨ ((q=0) ∨ (q=1))) |⟶ (path_term((phi)p;
(u)p+;
((a)sigma)p+;
((b)sigma)p+;
q))[0(𝕀)]]}
28. ((((Path_A a b))sigma)[1(𝕀)])p
= (H.𝕀 ⊢ Path_(((A)sigma)[1(𝕀)])p (((a)sigma)[1(𝕀)])p (((b)sigma)[1(𝕀)])p)
∈ {H.𝕀 ⊢ _}
29. {H.𝕀 ⊢ _:(((A)sigma)[1(𝕀)])p[((phi)p ∨ ((q=0) ∨ (q=1)))
|⟶ path-term((phi)p;((u)[1(𝕀)])p;(((a)sigma)[1(𝕀)])p;(((b)sigma)[1(𝕀)])p;q)]} ∈ 𝕌{[i' | j']}
30. (comp ((cA)sigma)p+ [((phi)p ∨ ((q=0) ∨ (q=1))) ⊢→ path_term((phi)p; (u)p+; ((a)sigma)p+; ((b)sigma)p+; q)]
(a0)p @ q)tau+
= comp (((cA)sigma)p+)tau++ [(((phi)p ∨ ((q=0) ∨ (q=1))))tau+ ⊢→ (path_term((phi)p; (u)p+; ((a)sigma)p+; ((b)sigma)p+; q
))tau++] ((a0)p @ q)tau+
∈ {K.𝕀 ⊢ _:((((A)sigma)p+)tau++)[1(𝕀)][(((phi)p ∨ ((q=0) ∨ (q=1))))tau+ |⟶ ((path_term((phi)p;
(u)p+;
((a)sigma)p+;
((b)sigma)p+;
q))tau++)[1(𝕀)]]}
⊢ ((a0)tau)p @ q ~ ((a0)p @ q)tau+
Latex:
Latex:
.....equality.....
1. G : CubicalSet\{j\}
2. A : \{G \mvdash{} \_\}
3. a : \{G \mvdash{} \_:A\}
4. b : \{G \mvdash{} \_:A\}
5. cA : G \mvdash{} Compositon(A)
6. path\_comp(G;A;a;b;
cA) \mmember{} composition-function\{j:l,i:l\}(G;(Path\_A a b))
7. H : CubicalSet\{j\}
8. K : CubicalSet\{j\}
9. tau : K j{}\mrightarrow{} H
10. sigma : H.\mBbbI{} j{}\mrightarrow{} G
11. phi : \{H \mvdash{} \_:\mBbbF{}\}
12. u : \{H, phi.\mBbbI{} \mvdash{} \_:((Path\_A a b))sigma\}
13. a0 : \{H \mvdash{} \_:(((Path\_A a b))sigma)[0(\mBbbI{})][phi |{}\mrightarrow{} (u)[0(\mBbbI{})]]\}
14. \{H, phi.\mBbbI{} \mvdash{} \_:((Path\_A a b))sigma\} = \{H, phi.\mBbbI{} \mvdash{} \_:(Path\_(A)sigma (a)sigma (b)sigma)\}
15. a0 \mmember{} \{H \mvdash{} \_:(Path\_((A)sigma)[0(\mBbbI{})] ((a)sigma)[0(\mBbbI{})] ((b)sigma)[0(\mBbbI{})])\}
16. a0 @ 0(\mBbbI{}) \mmember{} \{H \mvdash{} \_:((A)sigma)[0(\mBbbI{})]\}
17. p+ \mmember{} H.\mBbbI{}.\mBbbI{} ij{}\mrightarrow{} H.\mBbbI{}
18. \mforall{}[u:\{H.\mBbbI{}, ((phi)p \mvee{} ((q=0) \mvee{} (q=1))).\mBbbI{} \mvdash{} \_:((A)sigma)p+\}].
\mforall{}[a0:\{H.\mBbbI{} \mvdash{} \_:(((A)sigma)p+)[0(\mBbbI{})][((phi)p \mvee{} ((q=0) \mvee{} (q=1))) |{}\mrightarrow{} (u)[0(\mBbbI{})]]\}].
(comp ((cA)sigma)p+ [((phi)p \mvee{} ((q=0) \mvee{} (q=1))) \mvdash{}\mrightarrow{} u] a0
\mmember{} \{H.\mBbbI{} \mvdash{} \_:(((A)sigma)[1(\mBbbI{})])p[((phi)p \mvee{} ((q=0) \mvee{} (q=1))) |{}\mrightarrow{} (u)[1(\mBbbI{})]]\})
19. (u)p+ \mmember{} \{H.\mBbbI{}.\mBbbI{}, ((phi)p)p \mvdash{} \_:(((Path\_A a b))sigma)p+\}
20. (u)p+ \mmember{} \{H.\mBbbI{}, (phi)p.\mBbbI{} \mvdash{} \_:(((Path\_A a b))sigma)p+\}
21. \{H.\mBbbI{}.\mBbbI{} \mvdash{} \_:((A)sigma)p+\} \msubseteq{}r \{H.\mBbbI{}, (phi)p.\mBbbI{} \mvdash{} \_:((A)sigma)p+\}
22. \{H.\mBbbI{}.\mBbbI{} \mvdash{} \_:((A)sigma)p+\} \msubseteq{}r \{H.\mBbbI{}, (phi)p.\mBbbI{} \mvdash{} \_:((A)sigma)p+\}
23. ((b)sigma)p+ \mmember{} \{H.\mBbbI{}.\mBbbI{} \mvdash{} \_:((A)sigma)p+\}
24. ((a)sigma)p+ \mmember{} \{H.\mBbbI{}.\mBbbI{} \mvdash{} \_:((A)sigma)p+\}
25. (u)p+ \mmember{} \{H.\mBbbI{}, (phi)p.\mBbbI{} \mvdash{} \_:(Path\_((A)sigma)p+ ((a)sigma)p+ ((b)sigma)p+)\}
26. path\_term((phi)p; (u)p+; ((a)sigma)p+; ((b)sigma)p+; q)
\mmember{} \{H.\mBbbI{}, ((phi)p \mvee{} ((q=0) \mvee{} (q=1))).\mBbbI{} \mvdash{} \_:((A)sigma)p+\}
27. (a0)p @ q \mmember{} \{H.\mBbbI{} \mvdash{} \_:(((A)sigma)p+)[0(\mBbbI{})][((phi)p \mvee{} ((q=0) \mvee{} (q=1)))
|{}\mrightarrow{} (path\_term((phi)p; (u)p+; ((a)sigma)p+; ((b)sigma)p+; q))[0(\mBbbI{})]]\}
28. ((((Path\_A a b))sigma)[1(\mBbbI{})])p
= (H.\mBbbI{} \mvdash{} Path\_(((A)sigma)[1(\mBbbI{})])p (((a)sigma)[1(\mBbbI{})])p (((b)sigma)[1(\mBbbI{})])p)
29. \{H.\mBbbI{} \mvdash{} \_:(((A)sigma)[1(\mBbbI{})])p[((phi)p \mvee{} ((q=0) \mvee{} (q=1)))
|{}\mrightarrow{} path-term((phi)p;((u)[1(\mBbbI{})])p;(((a)sigma)[1(\mBbbI{})])p;(((b)sigma)[1(\mBbbI{})])p;q)]\}
\mmember{} \mBbbU{}\{[i' | j']\}
30. (comp ((cA)sigma)p+ [((phi)p \mvee{} ((q=0) \mvee{} (q=1))) \mvdash{}\mrightarrow{} path\_term((phi)p;
(u)p+;
((a)sigma)p+;
((b)sigma)p+;
q)] (a0)p @ q)tau+
= comp (((cA)sigma)p+)tau++ [(((phi)p \mvee{} ((q=0) \mvee{} (q=1))))tau+ \mvdash{}\mrightarrow{} (path\_term((phi)p;
(u)p+;
((a)sigma)p+;
((b)sigma)p+;
q))tau++]
((a0)p @ q)tau+
\mvdash{} comp ((cA)sigma o tau+)p+ [(((phi)tau)p \mvee{} ((q=0) \mvee{} (q=1))) \mvdash{}\mrightarrow{} path\_term(((phi)tau)p;
((u)tau+)p+;
((a)sigma o tau+)p+;
((b)sigma o tau+)p+;
q)] ((a0)tau)p @ q
\msim{} comp (((cA)sigma)p+)tau++ [(((phi)p \mvee{} ((q=0) \mvee{} (q=1))))tau+ \mvdash{}\mrightarrow{} (path\_term((phi)p;
(u)p+;
((a)sigma)p+;
((b)sigma)p+;
q))tau++]
((a0)p @ q)tau+
By
Latex:
(EqCD THEN Try (Trivial))
Home
Index