Step
*
1
1
1
1
2
1
2
3
of Lemma
glue-comp_wf2
.....subterm..... T:t
3:n
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. cA : G +⊢ Compositon(A)
4. phi : {G ⊢ _:𝔽}
5. T : {G, phi ⊢ _}
6. cT : G, phi +⊢ Compositon(T)
7. f : {G, phi ⊢ _:Equiv(T;A)}
8. comp(Glue [phi ⊢→ (T, f)] A) ∈ composition-function{j:l,i:l}(G;Glue [phi ⊢→ (T;equiv-fun(f))] A)
9. H : CubicalSet{j}
10. K : CubicalSet{j}
11. tau : K j⟶ H
12. sigma : H.𝕀 j⟶ G
13. psi : {H ⊢ _:𝔽}
14. b : {H, psi.𝕀 ⊢ _:(Glue [phi ⊢→ (T;equiv-fun(f))] A)sigma}
15. b0 : {H ⊢ _:((Glue [phi ⊢→ (T;equiv-fun(f))] A)sigma)[0(𝕀)]}
16. (b)[0(𝕀)] = b0 ∈ {H, psi ⊢ _:((Glue [phi ⊢→ (T;equiv-fun(f))] A)sigma)[0(𝕀)]}
17. G ⊢ Glue [phi ⊢→ (T;equiv-fun(f))] A
18. (Glue [phi ⊢→ (T;equiv-fun(f))] A)sigma
= H.𝕀 ⊢ Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma
∈ {H.𝕀 ⊢ _}
19. b ∈ {H.𝕀, (psi)p ⊢ _:Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma}
20. (phi)sigma ∈ {H.𝕀 ⊢ _:𝔽}
21. (equiv-fun(f))sigma ∈ {H.𝕀, (phi)sigma ⊢ _:((T)sigma ⟶ (A)sigma)}
22. {H.𝕀, (phi)sigma ⊢ _} ⊆r {H.𝕀, (psi)p, (phi)sigma ⊢ _}
23. H, ((phi)sigma)[0(𝕀)] ⊢ ((T)sigma)[0(𝕀)]
24. ((equiv-fun(f))sigma)[0(𝕀)] ∈ {H, ((phi)sigma)[0(𝕀)] ⊢ _:(((T ⟶ A))sigma)[0(𝕀)]}
25. ((equiv-fun(f))sigma)[0(𝕀)] ∈ {H, ((phi)sigma)[0(𝕀)] ⊢ _:(((T)sigma)[0(𝕀)] ⟶ ((A)sigma)[0(𝕀)])}
26. sub_cubical_set{j:l}(H, (∀ (phi)sigma), psi.𝕀; H.𝕀, (psi)p, (phi)sigma)
27. H, (∀ (phi)sigma).𝕀 ⊢ (T)sigma
28. H.𝕀, (phi)sigma +⊢ Compositon((T)sigma) ⊆r H, (∀ (phi)sigma).𝕀 +⊢ Compositon((T)sigma)
29. H.𝕀, (phi)sigma +⊢ Compositon((A)sigma) ⊆r H, (∀ (phi)sigma).𝕀 +⊢ Compositon((A)sigma)
30. H.𝕀, (psi)p, (phi)sigma ⊢ (T)sigma
31. H, (∀ (phi)sigma) ⊢ ((T)sigma)[1(𝕀)]
32. {H, ((phi)sigma)[1(𝕀)] ⊢ _} ⊆r {H, (∀ (phi)sigma) ⊢ _}
33. H, (∀ (phi)sigma) ⊢ ((T)sigma)[1(𝕀)]
34. unglue(b) ∈ {H.𝕀, (psi)p ⊢ _:(A)sigma[(phi)sigma |⟶ app((equiv-fun(f))sigma; b)]}
35. unglue(b0) ∈ {H ⊢ _:((A)sigma)[0(𝕀)][((phi)sigma)[0(𝕀)] |⟶ app(((equiv-fun(f))sigma)[0(𝕀)]; b0)]}
36. (cT)sigma ∈ H, (∀ (phi)sigma).𝕀 +⊢ Compositon((T)sigma)
37. (cA)sigma ∈ H, (∀ (phi)sigma).𝕀 +⊢ Compositon((A)sigma)
38. b0 ∈ {H, ((phi)sigma)[0(𝕀)] ⊢ _:((T)sigma)[0(𝕀)]}
39. b ∈ {H.𝕀, (psi)p, (phi)sigma ⊢ _:(T)sigma}
40. app((equiv-fun(f))sigma; b) ∈ {H.𝕀, (psi)p, (phi)sigma ⊢ _:(A)sigma}
41. H, ((phi)sigma)[1(𝕀)] ⊢ ((T)sigma)[1(𝕀)]
42. {H, ((phi)sigma)[1(𝕀)] ⊢ _} ⊆r {H, (∀ (phi)sigma) ⊢ _}
43. H, (∀ (phi)sigma) ⊢ ((T)sigma)[1(𝕀)]
44. a : {H.𝕀, (psi)p ⊢ _:(A)sigma[(phi)sigma |⟶ app((equiv-fun(f))sigma; b)]}
45. unglue(b) = a ∈ {H.𝕀, (psi)p ⊢ _:(A)sigma[(phi)sigma |⟶ app((equiv-fun(f))sigma; b)]}
46. a0 : {H ⊢ _:((A)sigma)[0(𝕀)][((phi)sigma)[0(𝕀)] |⟶ app(((equiv-fun(f))sigma)[0(𝕀)]; b0)]}
47. unglue(b0) = a0 ∈ {H ⊢ _:((A)sigma)[0(𝕀)][((phi)sigma)[0(𝕀)] |⟶ app(((equiv-fun(f))sigma)[0(𝕀)]; b0)]}
48. a0 ∈ {H ⊢ _:((A)sigma)[0(𝕀)]}
49. (b)[0(𝕀)] = b0 ∈ {H, psi ⊢ _:((Glue [phi ⊢→ (T;equiv-fun(f))] A)sigma)[0(𝕀)]}
50. partial-term-0(H;unglue(b)) = unglue(b0) ∈ {H, psi ⊢ _:((A)sigma)[0(𝕀)]}
51. z : {H ⊢ _:((A)sigma)[0(𝕀)]}
52. app(((equiv-fun(f))sigma)[0(𝕀)]; b0) = z ∈ {H, ((phi)sigma)[0(𝕀)] ⊢ _:((A)sigma)[0(𝕀)]}
⊢ a0 ∈ {H, psi ⊢ _:((A)sigma)[0(𝕀)]}
BY
{ (DoSubsume THEN Auto) }
Latex:
Latex:
.....subterm..... T:t
3:n
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 : G, phi +\mvdash{} Compositon(T)
7. f : \{G, phi \mvdash{} \_:Equiv(T;A)\}
8. comp(Glue [phi \mvdash{}\mrightarrow{} (T, f)] A) \mmember{} composition-function\{j:l,i:l\}(G;Glue [phi \mvdash{}\mrightarrow{} (T;equiv-fun(f))] A)
9. H : CubicalSet\{j\}
10. K : CubicalSet\{j\}
11. tau : K j{}\mrightarrow{} H
12. sigma : H.\mBbbI{} j{}\mrightarrow{} G
13. psi : \{H \mvdash{} \_:\mBbbF{}\}
14. b : \{H, psi.\mBbbI{} \mvdash{} \_:(Glue [phi \mvdash{}\mrightarrow{} (T;equiv-fun(f))] A)sigma\}
15. b0 : \{H \mvdash{} \_:((Glue [phi \mvdash{}\mrightarrow{} (T;equiv-fun(f))] A)sigma)[0(\mBbbI{})]\}
16. (b)[0(\mBbbI{})] = b0
17. G \mvdash{} Glue [phi \mvdash{}\mrightarrow{} (T;equiv-fun(f))] A
18. (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
19. b \mmember{} \{H.\mBbbI{}, (psi)p \mvdash{} \_:Glue [(phi)sigma \mvdash{}\mrightarrow{} ((T)sigma;(equiv-fun(f))sigma)] (A)sigma\}
20. (phi)sigma \mmember{} \{H.\mBbbI{} \mvdash{} \_:\mBbbF{}\}
21. (equiv-fun(f))sigma \mmember{} \{H.\mBbbI{}, (phi)sigma \mvdash{} \_:((T)sigma {}\mrightarrow{} (A)sigma)\}
22. \{H.\mBbbI{}, (phi)sigma \mvdash{} \_\} \msubseteq{}r \{H.\mBbbI{}, (psi)p, (phi)sigma \mvdash{} \_\}
23. H, ((phi)sigma)[0(\mBbbI{})] \mvdash{} ((T)sigma)[0(\mBbbI{})]
24. ((equiv-fun(f))sigma)[0(\mBbbI{})] \mmember{} \{H, ((phi)sigma)[0(\mBbbI{})] \mvdash{} \_:(((T {}\mrightarrow{} A))sigma)[0(\mBbbI{})]\}
25. ((equiv-fun(f))sigma)[0(\mBbbI{})] \mmember{} \{H, ((phi)sigma)[0(\mBbbI{})] \mvdash{} \_:(((T)sigma)[0(\mBbbI{})] {}\mrightarrow{} ((A)sigma)[0(\mBbbI{})])\}
26. sub\_cubical\_set\{j:l\}(H, (\mforall{} (phi)sigma), psi.\mBbbI{}; H.\mBbbI{}, (psi)p, (phi)sigma)
27. H, (\mforall{} (phi)sigma).\mBbbI{} \mvdash{} (T)sigma
28. H.\mBbbI{}, (phi)sigma +\mvdash{} Compositon((T)sigma) \msubseteq{}r H, (\mforall{} (phi)sigma).\mBbbI{} +\mvdash{} Compositon((T)sigma)
29. H.\mBbbI{}, (phi)sigma +\mvdash{} Compositon((A)sigma) \msubseteq{}r H, (\mforall{} (phi)sigma).\mBbbI{} +\mvdash{} Compositon((A)sigma)
30. H.\mBbbI{}, (psi)p, (phi)sigma \mvdash{} (T)sigma
31. H, (\mforall{} (phi)sigma) \mvdash{} ((T)sigma)[1(\mBbbI{})]
32. \{H, ((phi)sigma)[1(\mBbbI{})] \mvdash{} \_\} \msubseteq{}r \{H, (\mforall{} (phi)sigma) \mvdash{} \_\}
33. H, (\mforall{} (phi)sigma) \mvdash{} ((T)sigma)[1(\mBbbI{})]
34. unglue(b) \mmember{} \{H.\mBbbI{}, (psi)p \mvdash{} \_:(A)sigma[(phi)sigma |{}\mrightarrow{} app((equiv-fun(f))sigma; b)]\}
35. unglue(b0) \mmember{} \{H \mvdash{} \_:((A)sigma)[0(\mBbbI{})][((phi)sigma)[0(\mBbbI{})]
|{}\mrightarrow{} app(((equiv-fun(f))sigma)[0(\mBbbI{})]; b0)]\}
36. (cT)sigma \mmember{} H, (\mforall{} (phi)sigma).\mBbbI{} +\mvdash{} Compositon((T)sigma)
37. (cA)sigma \mmember{} H, (\mforall{} (phi)sigma).\mBbbI{} +\mvdash{} Compositon((A)sigma)
38. b0 \mmember{} \{H, ((phi)sigma)[0(\mBbbI{})] \mvdash{} \_:((T)sigma)[0(\mBbbI{})]\}
39. b \mmember{} \{H.\mBbbI{}, (psi)p, (phi)sigma \mvdash{} \_:(T)sigma\}
40. app((equiv-fun(f))sigma; b) \mmember{} \{H.\mBbbI{}, (psi)p, (phi)sigma \mvdash{} \_:(A)sigma\}
41. H, ((phi)sigma)[1(\mBbbI{})] \mvdash{} ((T)sigma)[1(\mBbbI{})]
42. \{H, ((phi)sigma)[1(\mBbbI{})] \mvdash{} \_\} \msubseteq{}r \{H, (\mforall{} (phi)sigma) \mvdash{} \_\}
43. H, (\mforall{} (phi)sigma) \mvdash{} ((T)sigma)[1(\mBbbI{})]
44. a : \{H.\mBbbI{}, (psi)p \mvdash{} \_:(A)sigma[(phi)sigma |{}\mrightarrow{} app((equiv-fun(f))sigma; b)]\}
45. unglue(b) = a
46. a0 : \{H \mvdash{} \_:((A)sigma)[0(\mBbbI{})][((phi)sigma)[0(\mBbbI{})] |{}\mrightarrow{} app(((equiv-fun(f))sigma)[0(\mBbbI{})]; b0)]\}
47. unglue(b0) = a0
48. a0 \mmember{} \{H \mvdash{} \_:((A)sigma)[0(\mBbbI{})]\}
49. (b)[0(\mBbbI{})] = b0
50. partial-term-0(H;unglue(b)) = unglue(b0)
51. z : \{H \mvdash{} \_:((A)sigma)[0(\mBbbI{})]\}
52. app(((equiv-fun(f))sigma)[0(\mBbbI{})]; b0) = z
\mvdash{} a0 \mmember{} \{H, psi \mvdash{} \_:((A)sigma)[0(\mBbbI{})]\}
By
Latex:
(DoSubsume THEN Auto)
Home
Index