Step
*
1
1
1
1
1
2
2
2
1
1
2
2
1
1
1
1
1
2
2
1
2
1
1
1
of Lemma
glue-comp-agrees
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. ∀H,K:ij⊢. ∀tau:K ij⟶ H. ∀sigma:H.𝕀 ij⟶ G, phi. ∀phi@0:{H ⊢ _:𝔽}. ∀u:{H, phi@0.𝕀 ⊢ _:(T)sigma}.
∀a0:{H ⊢ _:((T)sigma)[0(𝕀)][phi@0 |⟶ (u)[0(𝕀)]]}.
((cT H sigma phi@0 u a0)tau
= (cT K sigma o tau+ (phi@0)tau (u)tau+ (a0)tau)
∈ {K ⊢ _:(((T)sigma)[1(𝕀)])tau[(phi@0)tau |⟶ ((u)[1(𝕀)])tau]})
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. s1 : H.𝕀 ij⟶ G, phi
39. p1 : {H ⊢ _:𝔽}
40. u : {H, p1.𝕀 ⊢ _:(T)s1}
41. a1 : {H ⊢ _:((T)s1)[0(𝕀)][p1 |⟶ (u)[0(𝕀)]]}
42. (cT H, 1(𝔽) s1 p1 u a1)1(H)
= (cT H s1 o 1(H)+ (p1)1(H) (u)1(H)+ (a1)1(H))
∈ {H ⊢ _:(((T)s1)[1(𝕀)])1(H)[(p1)1(H) |⟶ ((u)[1(𝕀)])1(H)]}
43. (cT H, 1(𝔽) s1 p1 u a1) = (cT H, (∀ (phi)sigma) s1 p1 u a1) ∈ {H, 1(𝔽) ⊢ _:((T)s1)[1(𝕀)][p1 |⟶ (u)[1(𝕀)]]}
44. x : {H, 1(𝔽) ⊢ _:((T)s1)[1(𝕀)]}
45. (u)[1(𝕀)] = x ∈ {H, 1(𝔽), p1 ⊢ _:((T)s1)[1(𝕀)]}
46. x = x ∈ {H, 1(𝔽) ⊢ _:((T)s1)[1(𝕀)]}
⊢ {H, 1(𝔽) ⊢ _:((T)s1)[1(𝕀)]} ⊆r {H ⊢ _:((T)s1)[1(𝕀)]}
BY
{ ((Subst' [1(𝕀)] ~ [1(𝕀)] 0 THENA (CsmUnfolding THEN Auto)) THEN BLemma `subset-cubical-term` THEN Auto) }
Latex:
Latex:
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. \mforall{}H,K:ij\mvdash{}. \mforall{}tau:K ij{}\mrightarrow{} H. \mforall{}sigma:H.\mBbbI{} ij{}\mrightarrow{} G, phi. \mforall{}phi@0:\{H \mvdash{} \_:\mBbbF{}\}. \mforall{}u:\{H, phi@0.\mBbbI{} \mvdash{} \_:(T)sigma\}.
\mforall{}a0:\{H \mvdash{} \_:((T)sigma)[0(\mBbbI{})][phi@0 |{}\mrightarrow{} (u)[0(\mBbbI{})]]\}.
((cT H sigma phi@0 u a0)tau = (cT K sigma o tau+ (phi@0)tau (u)tau+ (a0)tau))
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. s1 : H.\mBbbI{} ij{}\mrightarrow{} G, phi
39. p1 : \{H \mvdash{} \_:\mBbbF{}\}
40. u : \{H, p1.\mBbbI{} \mvdash{} \_:(T)s1\}
41. a1 : \{H \mvdash{} \_:((T)s1)[0(\mBbbI{})][p1 |{}\mrightarrow{} (u)[0(\mBbbI{})]]\}
42. (cT H, 1(\mBbbF{}) s1 p1 u a1)1(H) = (cT H s1 o 1(H)+ (p1)1(H) (u)1(H)+ (a1)1(H))
43. (cT H, 1(\mBbbF{}) s1 p1 u a1) = (cT H, (\mforall{} (phi)sigma) s1 p1 u a1)
44. x : \{H, 1(\mBbbF{}) \mvdash{} \_:((T)s1)[1(\mBbbI{})]\}
45. (u)[1(\mBbbI{})] = x
46. x = x
\mvdash{} \{H, 1(\mBbbF{}) \mvdash{} \_:((T)s1)[1(\mBbbI{})]\} \msubseteq{}r \{H \mvdash{} \_:((T)s1)[1(\mBbbI{})]\}
By
Latex:
((Subst' [1(\mBbbI{})] \msim{} [1(\mBbbI{})] 0 THENA (CsmUnfolding THEN Auto))
THEN BLemma `subset-cubical-term`
THEN Auto)
Home
Index