Proof of Nuprl Lemma : glue-comp

Step * 1 2 1 1 2 1 2 2 2 1 2 1 3 1 1 2 1 3 2 1 1 1 1 2 2 2 1 1 2 1 2 2 2 2 2 1 2 1 1 1 of Lemma glue-comp_wf2

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(𝕀)][psi |⟶ (b)[0(𝕀)]]}
16. G ⊢ Glue [phi ⊢→ (T;equiv-fun(f))] A
17. (Glue [phi ⊢→ (T;equiv-fun(f))] A)sigma
= H.𝕀 ⊢ Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma
∈ {H.𝕀 ⊢ _}
18. b ∈ {H.𝕀, (psi)p ⊢ _:Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma}
19. (phi)sigma ∈ {H.𝕀 ⊢ _:𝔽}
20. (equiv-fun(f))sigma ∈ {H.𝕀, (phi)sigma ⊢ _:((T)sigma ⟶ (A)sigma)}
21. {H.𝕀, (phi)sigma ⊢ _} ⊆r {H.𝕀, (psi)p, (phi)sigma ⊢ _}
22. H, ((phi)sigma)[0(𝕀)] ⊢ ((T)sigma)[0(𝕀)]
23. ((equiv-fun(f))sigma)[0(𝕀)] ∈ {H, ((phi)sigma)[0(𝕀)] ⊢ _:(((T ⟶ A))sigma)[0(𝕀)]}

24. ((equiv-fun(f))sigma)[0(𝕀)] ∈ {H, ((phi)sigma)[0(𝕀)] ⊢ _:(((T)sigma)[0(𝕀)] ⟶ ((A)sigma)[0(𝕀)])}

25. sub_cubical_set{j:l}(H, (∀ (phi)sigma), psi.𝕀; H.𝕀, (psi)p, (phi)sigma)
26. H, (∀ (phi)sigma).𝕀 ⊢ (T)sigma
27. H.𝕀, (phi)sigma +⊢ Compositon((T)sigma) ⊆r H, (∀ (phi)sigma).𝕀 +⊢ Compositon((T)sigma)
28. H.𝕀, (phi)sigma +⊢ Compositon((A)sigma) ⊆r H, (∀ (phi)sigma).𝕀 +⊢ Compositon((A)sigma)
29. H.𝕀, (psi)p, (phi)sigma ⊢ (T)sigma
30. H, (∀ (phi)sigma) ⊢ ((T)sigma)[1(𝕀)]
31. {H, ((phi)sigma)[1(𝕀)] ⊢ _} ⊆r {H, (∀ (phi)sigma) ⊢ _}
32. H, (∀ (phi)sigma) ⊢ ((T)sigma)[1(𝕀)]
33. unglue(b) ∈ {H.𝕀, (psi)p ⊢ _:(A)sigma[(phi)sigma |⟶ app((equiv-fun(f))sigma; b)]}

34. unglue(b0) ∈ {H ⊢ _:((A)sigma)[0(𝕀)][((phi)sigma)[0(𝕀)] |⟶ app(((equiv-fun(f))sigma)[0(𝕀)]; b0)]}

35. (cT)sigma ∈ H, (∀ (phi)sigma).𝕀 +⊢ Compositon((T)sigma)
36. (cA)sigma ∈ H, (∀ (phi)sigma).𝕀 +⊢ Compositon((A)sigma)
37. b0 ∈ {H, ((phi)sigma)[0(𝕀)] ⊢ _:((T)sigma)[0(𝕀)]}
38. b ∈ {H.𝕀, (psi)p, (phi)sigma ⊢ _:(T)sigma}
39. app((equiv-fun(f))sigma; b) ∈ {H.𝕀, (psi)p, (phi)sigma ⊢ _:(A)sigma}
40. H, ((phi)sigma)[1(𝕀)] ⊢ ((T)sigma)[1(𝕀)]
41. {H, ((phi)sigma)[1(𝕀)] ⊢ _} ⊆r {H, (∀ (phi)sigma) ⊢ _}
42. H, (∀ (phi)sigma) ⊢ ((T)sigma)[1(𝕀)]
43. a : {H.𝕀, (psi)p ⊢ _:(A)sigma[(phi)sigma |⟶ app((equiv-fun(f))sigma; b)]}
44. unglue(b) = a ∈ {H.𝕀, (psi)p ⊢ _:(A)sigma[(phi)sigma |⟶ app((equiv-fun(f))sigma; b)]}
45. a0 : {H ⊢ _:((A)sigma)[0(𝕀)][((phi)sigma)[0(𝕀)] |⟶ app(((equiv-fun(f))sigma)[0(𝕀)]; b0)]}

46. unglue(b0) = a0 ∈ {H ⊢ _:((A)sigma)[0(𝕀)][((phi)sigma)[0(𝕀)] |⟶ app(((equiv-fun(f))sigma)[0(𝕀)]; b0)]}

47. a0 ∈ {H ⊢ _:((A)sigma)[0(𝕀)][psi |⟶ a[0]]}
48. (comp (cA)sigma [psi ⊢→ a] a0)tau
= comp ((cA)sigma)tau+ [(psi)tau ⊢→ (a)tau+] (a0)tau
∈ {K ⊢ _:(((A)sigma)tau+)[1(𝕀)][(psi)tau |⟶ ((a)tau+)[1(𝕀)]]}
49. comp (cA)sigma [psi ⊢→ a] a0 ∈ {H ⊢ _:((A)sigma)[1(𝕀)][psi |⟶ a[1]]}
50. a'1 : {H ⊢ _:((A)sigma)[1(𝕀)][psi |⟶ a[1]]}
51. comp (cA)sigma [psi ⊢→ a] a0 = a'1 ∈ {H ⊢ _:((A)sigma)[1(𝕀)][psi |⟶ a[1]]}
52. ((psi)p)tau+ ∈ {K.𝕀 ⊢ _:𝔽}
53. {K ⊢ _:(((A)sigma)tau+)[1(𝕀)][(psi)tau |⟶ ((a)tau+)[1(𝕀)]]} ∈ 𝕌{[i' | j']}
54. aa'1 : {K ⊢ _:(((A)sigma)tau+)[1(𝕀)][(psi)tau |⟶ ((a)tau+)[1(𝕀)]]}
55. comp ((cA)sigma)tau+ [(psi)tau ⊢→ (a)tau+] (a0)tau
= aa'1
∈ {K ⊢ _:(((A)sigma)tau+)[1(𝕀)][(psi)tau |⟶ ((a)tau+)[1(𝕀)]]}
56. (a'1)tau = aa'1 ∈ {K ⊢ _:(((A)sigma)tau+)[1(𝕀)][(psi)tau |⟶ ((a)tau+)[1(𝕀)]]}
57. b ∈ {H, (∀ (phi)sigma), psi.𝕀 ⊢ _:(T)sigma}
58. (b)[0(𝕀)] = b0 ∈ {H, (∀ (phi)sigma), psi ⊢ _:((T)sigma)[0(𝕀)]}
59. b0 ∈ {H, (∀ (phi)sigma) ⊢ _:((T)sigma)[0(𝕀)][psi |⟶ (b)[0(𝕀)]]}

60. comp (cT)sigma [psi ⊢→ b] b0 ∈ {H, (∀ (phi)sigma) ⊢ _:((T)sigma)[1(𝕀)][psi |⟶ (b)[1(𝕀)]]}

61. (comp (cT)sigma [psi ⊢→ b] b0)tau
= comp ((cT)sigma)tau+ [(psi)tau ⊢→ (b)tau+] (b0)tau
∈ {K, ((∀ (phi)sigma))tau ⊢ _:(((T)sigma)tau+)[1(𝕀)][(psi)tau |⟶ ((b)tau+)[1(𝕀)]]}
62. H, ((phi)sigma)[1(𝕀)] ⊢ ((T)sigma)[1(𝕀)]
63. (b)[1(𝕀)] ∈ {H, ((phi)sigma)[1(𝕀)], psi ⊢ _:((T)sigma)[1(𝕀)]}
64. {H, ((phi)sigma)[1(𝕀)] ⊢ _} ⊆r {H, (∀ (phi)sigma) ⊢ _}
65. H, (∀ (phi)sigma) ⊢ ((T)sigma)[1(𝕀)]
66. (b)[1(𝕀)] ∈ {H, (∀ (phi)sigma), psi ⊢ _:((T)sigma)[1(𝕀)]}
67. {H, (∀ (phi)sigma) ⊢ _:((T)sigma)[1(𝕀)][psi |⟶ (b)[1(𝕀)]]} ∈ 𝕌{[i' | j']}
68. sub_cubical_set{j:l}(K, ((∀ (phi)sigma))tau.𝕀; K.𝕀, (phi)sigma o tau+)
69. sub_cubical_set{j:l}(K, ((∀ (phi)sigma))tau.𝕀; K.𝕀, ((phi)sigma)tau+)
70. {K.𝕀, ((phi)sigma)tau+ ⊢ _} ⊆r {K, ((∀ (phi)sigma))tau.𝕀 ⊢ _}
71. K, ((∀ (phi)sigma))tau.𝕀 ⊢ ((T)sigma)tau+
72. (comp (cT)sigma [psi ⊢→ b] b0)tau
= comp (cT)sigma o tau+ [(psi)tau ⊢→ (b)tau+] (b0)tau
∈ {K, ((∀ (phi)sigma))tau ⊢ _:(((T)sigma)tau+)[1(𝕀)][(psi)tau |⟶ ((b)tau+)[1(𝕀)]]}

73. {K, ((∀ (phi)sigma))tau ⊢ _:(((T)sigma)tau+)[1(𝕀)][(psi)tau |⟶ ((b)tau+)[1(𝕀)]]} ∈ 𝕌{[i | j']}

74. t'1 : {H, (∀ (phi)sigma) ⊢ _:((T)sigma)[1(𝕀)][psi |⟶ (b)[1(𝕀)]]}

75. comp (cT)sigma [psi ⊢→ b] b0 = t'1 ∈ {H, (∀ (phi)sigma) ⊢ _:((T)sigma)[1(𝕀)][psi |⟶ (b)[1(𝕀)]]}

76. tt'1 : {K, ((∀ (phi)sigma))tau ⊢ _:(((T)sigma)tau+)[1(𝕀)][(psi)tau |⟶ ((b)tau+)[1(𝕀)]]}
77. comp (cT)sigma o tau+ [(psi)tau ⊢→ (b)tau+] (b0)tau
= tt'1
∈ {K, ((∀ (phi)sigma))tau ⊢ _:(((T)sigma)tau+)[1(𝕀)][(psi)tau |⟶ ((b)tau+)[1(𝕀)]]}

78. (t'1)tau = tt'1 ∈ {K, ((∀ (phi)sigma))tau ⊢ _:(((T)sigma)tau+)[1(𝕀)][(psi)tau |⟶ ((b)tau+)[1(𝕀)]]}

79. (equiv-fun(f))sigma ∈ {H, (∀ (phi)sigma).𝕀 ⊢ _:((T)sigma ⟶ (A)sigma)}
80. b ∈ {H, (∀ (phi)sigma).𝕀, (psi)p ⊢ _:(T)sigma}
81. b0 ∈ {H, (∀ (phi)sigma) ⊢ _:((T)sigma)[0(𝕀)][psi |⟶ b[0]]}

82. pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma) ∈ {H, (∀ (phi)sigma) ⊢ _:((A)sigma)[1(𝕀)]}

83. partial-term-1(H, (∀ (phi)sigma);app((equiv-fun(f))sigma; b))
= pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma)
∈ {H, (∀ (phi)sigma), psi ⊢ _:((A)sigma)[1(𝕀)]}
84. (pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma))tau
= pres-c1(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;(b0)tau;((cA)sigma)tau+)

∈ {K, ((∀ (phi)sigma))tau ⊢ _:(((A)sigma)tau+)[1(𝕀)][(psi)tau |⟶ app(((equiv-fun(f))sigma)tau+; (b)tau+)[1]]}

85. pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma) ∈ {H, (∀ (phi)sigma) ⊢ _:((A)sigma)[1(𝕀)]}

86. partial-term-1(H, (∀ (phi)sigma);app((equiv-fun(f))sigma; b))
= pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma)
∈ {H, (∀ (phi)sigma), psi ⊢ _:((A)sigma)[1(𝕀)]}
87. (pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))tau
= pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;(b0)tau;((cT)sigma)tau+)

∈ {K, ((∀ (phi)sigma))tau ⊢ _:(((A)sigma)tau+)[1(𝕀)][(psi)tau |⟶ app(((equiv-fun(f))sigma)tau+; (b)tau+)[1]]}

88. app((equiv-fun(f))sigma; b)[1] ∈ {H, (∀ (phi)sigma), psi ⊢ _:((A)sigma)[1(𝕀)]}

89. {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))[psi

                           |⟶ <>((app((equiv-fun(f))sigma; b)[1])p)]} ∈ 𝕌{[i' | j']}

90. (equiv-fun(f))sigma ∈ {H, (∀ (phi)sigma).𝕀 ⊢ _:((T)sigma ⟶ (A)sigma)}
91. b ∈ {H, (∀ (phi)sigma).𝕀, (psi)p ⊢ _:(T)sigma}
92. b0 ∈ {H, (∀ (phi)sigma) ⊢ _:((T)sigma)[0(𝕀)][psi |⟶ b[0]]}
93. 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))[psi

|⟶ <>((app((equiv-fun(f))sigma; b)[1])p)]}
94. (pres (equiv-fun(f))sigma [psi ⊢→ b] b0)tau
= pres ((equiv-fun(f))sigma)tau+ [(psi)tau ⊢→ (b)tau+] (b0)tau
∈ {K, ((∀ (phi)sigma))tau ⊢ _:(Path_(((A)sigma)tau+)[1(𝕀)] pres-c1(K, ((∀ (phi)sigma))tau;(psi)tau;

                                                                   ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                   (b0)tau;((cA)sigma)tau+)

                                    pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

(b0)tau;((cT)sigma)tau+))}
95. ((equiv-fun(f))sigma)tau+ ∈ {K, ((∀ (phi)sigma))tau.𝕀 ⊢ _:(((T)sigma)tau+ ⟶ ((A)sigma)tau+)}

96. app(((equiv-fun(f))sigma)tau+; (b)tau+)[1] ∈ {K, ((∀ (phi)sigma))tau, (psi)tau ⊢ _:(((A)sigma)tau+)[1(𝕀)]}

97. pres-c1(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;(b0)tau;((cA)sigma)tau+)
∈ {K, ((∀ (phi)sigma))tau ⊢ _:(((A)sigma)tau+)[1(𝕀)]}
98. pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;(b0)tau;((cT)sigma)tau+)
∈ {K, ((∀ (phi)sigma))tau ⊢ _:(((A)sigma)tau+)[1(𝕀)]}
99. {K, ((∀ (phi)sigma))tau ⊢ _:(Path_(((A)sigma)tau+)[1(𝕀)] pres-c1(K, ((∀ (phi)sigma))tau;(psi)tau;

                                                                     ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                     (b0)tau;((cA)sigma)tau+)

                                      pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

                                              (b0)tau;((cT)sigma)tau+))} ∈ 𝕌{[i' | j']}

100. (pres (equiv-fun(f))sigma [psi ⊢→ b] b0)tau
= pres (equiv-fun(f))sigma o tau+ [(psi)tau ⊢→ (b)tau+] (b0)tau
∈ {K, ((∀ (phi)sigma))tau ⊢ _:(Path_(((A)sigma)tau+)[1(𝕀)] pres-c1(K, ((∀ (phi)sigma))tau;(psi)tau;

                                                                   ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                   (b0)tau;((cA)sigma)tau+)

                                    pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

(b0)tau;((cT)sigma)tau+))}

101. 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))[psi

|⟶ <>((app((equiv-fun(f))sigma; b)[1])p)]}
102. 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))[psi

|⟶ <>((app((equiv-fun(f))sigma; b)[1])p)]}

103. ww : {K, ((∀ (phi)sigma))tau ⊢ _:(Path_(((A)sigma)tau+)[1(𝕀)] pres-c1(K, ((∀ (phi)sigma))tau;(psi)tau;

                                                                           ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                           (b0)tau;((cA)sigma)tau+)

                                            pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

                                                    (b0)tau;((cT)sigma)tau+))}

104. pres (equiv-fun(f))sigma o tau+ [(psi)tau ⊢→ (b)tau+] (b0)tau
= ww
∈ {K, ((∀ (phi)sigma))tau ⊢ _:(Path_(((A)sigma)tau+)[1(𝕀)] pres-c1(K, ((∀ (phi)sigma))tau;(psi)tau;

                                                                   ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                   (b0)tau;((cA)sigma)tau+)

                                    pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

(b0)tau;((cT)sigma)tau+))}
105. (w)tau
= ww
∈ {K, ((∀ (phi)sigma))tau ⊢ _:(Path_(((A)sigma)tau+)[1(𝕀)] pres-c1(K, ((∀ (phi)sigma))tau;(psi)tau;

                                                                   ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                   (b0)tau;((cA)sigma)tau+)

                                    pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

(b0)tau;((cT)sigma)tau+))}
106. H, ((phi)sigma)[1(𝕀)] ⊢ ((T)sigma)[1(𝕀)]
107. (b)[1(𝕀)] ∈ {H, ((phi)sigma)[1(𝕀)], psi ⊢ _:((T)sigma)[1(𝕀)]}
108. H, (∀ (phi)sigma) ⊢ ((T)sigma)[1(𝕀)]
109. (b)[1(𝕀)] ∈ {H, (∀ (phi)sigma), psi ⊢ _:((T)sigma)[1(𝕀)]}
110. {H, (∀ (phi)sigma) ⊢ _:((T)sigma)[1(𝕀)][psi |⟶ (b)[1(𝕀)]]}
⊆r {H, ((phi)sigma)[1(𝕀)], (∀ (phi)sigma) ⊢ _:((T)sigma)[1(𝕀)][psi |⟶ (b)[1(𝕀)]]}
111. H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ ((T)sigma)[1(𝕀)]

112. (t'1 ∨ (b)[1(𝕀)]) ∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:((T)sigma)[1(𝕀)]}

113. ((t'1 ∨ (b)[1(𝕀)]))tau ∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _:(((T)sigma)[1(𝕀)])tau}

114. (tt'1 ∨ ((b)tau+)[1(𝕀)])
= ((t'1 ∨ (b)[1(𝕀)]))tau
∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _:(((T)sigma)[1(𝕀)])tau}

115. {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _:(((T)sigma)[1(𝕀)])tau} ∈ 𝕌{[i' | j']}

116. st : {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:((T)sigma)[1(𝕀)]}

117. (t'1 ∨ (b)[1(𝕀)]) = st ∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:((T)sigma)[1(𝕀)]}

118. stt : {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _:(((T)sigma)[1(𝕀)])tau}
119. (tt'1 ∨ ((b)tau+)[1(𝕀)])
= stt
∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _:(((T)sigma)[1(𝕀)])tau}

120. stt = (st)tau ∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _:(((T)sigma)[1(𝕀)])tau}

121. app(equiv-fun(((f)sigma)[1(𝕀)]); st) ∈ {H, ((∀ (phi)sigma) ∨ (((phi)sigma)[1(𝕀)] ∧ psi)) ⊢ _:((A)sigma)[1(𝕀)]}

122. H, ((∀ (phi)sigma) ∨ (((phi)sigma)[1(𝕀)] ∧ psi)) ⊢ (Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))

123. <>((app((equiv-fun(f))sigma; b)[1])p)

     ∈ {H, ((phi)sigma)[1(𝕀)], psi ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))}

124. sub_cubical_set{j:l}(H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi);
H, ((∀ (phi)sigma) ∨ (((phi)sigma)[1(𝕀)] ∧ psi)))

125. H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ (Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))

126. w ∈ {H, ((phi)sigma)[1(𝕀)], (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))

                                                    [psi |⟶ <>((app((equiv-fun(f))sigma; b)[1])p)]}

127. (w ∨ <>((app((equiv-fun(f))sigma; b)[1])p)) ∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _

                                                    :(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))}

128. {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _
:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))} ∈ 𝕌{[i' | j']}

129. ((w ∨ <>((app((equiv-fun(f))sigma; b)[1])p)))tau ∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _

                                                         :((Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]);

                                                                                          st)))tau}

130. ((w ∨ <>((app((equiv-fun(f))sigma; b)[1])p)))tau
= (ww ∨ <>((app((equiv-fun(f))sigma o tau+; (b)tau+)[1])p))
∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _
:((Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st)))tau}

131. sw : {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]);

                                                                                            st))}

132. (w ∨ <>((app((equiv-fun(f))sigma; b)[1])p))
= sw

∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))}

133. sww : {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _
            :((Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st)))tau}
134. (ww ∨ <>((app((equiv-fun(f))sigma o tau+; (b)tau+)[1])p))
= sww
∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _
   :((Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st)))tau}
135. (sw)tau
= sww
∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _
   :((Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st)))tau}

136. equiv-fun(((f)sigma)[1(𝕀)]) ∈ {H, ((phi)sigma)[1(𝕀)] ⊢ _:(((T)sigma)[1(𝕀)] ⟶ ((A)sigma)[1(𝕀)])}

137. 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(𝕀)])
     ∈ H, ((phi)sigma)[1(𝕀)] +⊢ Compositon(Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1))
138. H, ((phi)sigma)[1(𝕀)] +⊢ Compositon(Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1)) ∈ 𝕌{[i'' | j'']}
139. a'1 ∈ {H, ((phi)sigma)[1(𝕀)] ⊢ _:((A)sigma)[1(𝕀)]}
140. ((cA)sigma o [1(𝕀)] ∈ H, ((phi)sigma)[1(𝕀)] +⊢ Compositon(((A)sigma)[1(𝕀)]))
∧ ((cT)sigma o [1(𝕀)] ∈ H, ((phi)sigma)[1(𝕀)] +⊢ Compositon(((T)sigma)[1(𝕀)]))
141. (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(𝕀)]))tau

= fiber-comp(K, (((phi)sigma)[1(𝕀)])tau;(((T)sigma)[1(𝕀)])tau;(((A)sigma)[1(𝕀)])tau;(equiv-fun(((f)sigma)[1(𝕀)]))tau;

(a'1)tau;((cT)sigma o [1(𝕀)])tau;((cA)sigma o [1(𝕀)])tau)
∈ K, (((phi)sigma)[1(𝕀)])tau +⊢ Compositon(Fiber((equiv-fun(((f)sigma)[1(𝕀)]))tau;(a'1)tau))

142. K, (((phi)sigma)[1(𝕀)])tau +⊢ Compositon(Fiber((equiv-fun(((f)sigma)[1(𝕀)]))tau;(a'1)tau)) ∈ 𝕌{[i'' | j'']}

143. (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(𝕀)]))tau
= fiber-comp(K, ((phi)sigma o tau+)[1(𝕀)];((T)sigma o tau+)[1(𝕀)];((A)sigma o tau+)[1(𝕀)];

             equiv-fun(((f)sigma o tau+)[1(𝕀)]);aa'1;(cT)sigma o tau+ o [1(𝕀)];(cA)sigma o tau+ o [1(𝕀)])

∈ K, (((phi)sigma)[1(𝕀)])tau +⊢ Compositon(Fiber((equiv-fun(((f)sigma)[1(𝕀)]))tau;(a'1)tau))
144. cF : H, ((phi)sigma)[1(𝕀)] +⊢ Compositon(Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1))
145. 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))
146. cFF : K, (((phi)sigma)[1(𝕀)])tau +⊢ Compositon(Fiber((equiv-fun(((f)sigma)[1(𝕀)]))tau;(a'1)tau))
147. fiber-comp(K, ((phi)sigma o tau+)[1(𝕀)];((T)sigma o tau+)[1(𝕀)];((A)sigma o tau+)[1(𝕀)];

                equiv-fun(((f)sigma o tau+)[1(𝕀)]);aa'1;(cT)sigma o tau+ o [1(𝕀)];(cA)sigma o tau+ o [1(𝕀)])

= cFF
∈ K, (((phi)sigma)[1(𝕀)])tau +⊢ Compositon(Fiber((equiv-fun(((f)sigma)[1(𝕀)]))tau;(a'1)tau))

148. (cF)tau = cFF ∈ K, (((phi)sigma)[1(𝕀)])tau +⊢ Compositon(Fiber((equiv-fun(((f)sigma)[1(𝕀)]))tau;(a'1)tau))

149. a'1 ∈ {H, ((phi)sigma)[1(𝕀)] ⊢ _:((A)sigma)[1(𝕀)]}
150. ((f)sigma)[1(𝕀)] ∈ {H, ((phi)sigma)[1(𝕀)] ⊢ _:Equiv(((T)sigma)[1(𝕀)];((A)sigma)[1(𝕀)])}
151. equiv ((f)sigma)[1(𝕀)] [((∀ (phi)sigma) ∨ psi) ⊢→ (st, sw)] a'1

     ∈ {H, ((phi)sigma)[1(𝕀)] ⊢ _:Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1)[((∀ (phi)sigma) ∨ psi) |⟶ fiber-point(st;sw)]}

152. (equiv ((f)sigma)[1(𝕀)] [((∀ (phi)sigma) ∨ psi) ⊢→ (st, sw)] a'1)tau
= equiv (((f)sigma)[1(𝕀)])tau [(((∀ (phi)sigma) ∨ psi))tau ⊢→ ((st)tau, (sw)tau)] (a'1)tau

∈ {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

|⟶ fiber-point((st)tau;(sw)tau)]}

153. fiber-point(st;sw) ∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1)}

154. equiv-fun((((f)sigma)[1(𝕀)])tau)
∈ {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:((((T)sigma)[1(𝕀)])tau ⟶ (((A)sigma)[1(𝕀)])tau)}
155. K, (((phi)sigma)[1(𝕀)])tau ⊢ Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)
∧ (fiber-point((st)tau;(sw)tau) ∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _

                                   :Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)})

156. {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

                                     |⟶ fiber-point((st)tau;(sw)tau)]} ∈ 𝕌{[i' | j']}

157. (equiv ((f)sigma)[1(𝕀)] [((∀ (phi)sigma) ∨ psi) ⊢→ (st, sw)] a'1)tau
= equiv ((f)sigma o tau+)[1(𝕀)] [((∀ (phi)sigma o tau+) ∨ (psi)tau) ⊢→ (stt, sww)] aa'1

∈ {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

|⟶ fiber-point((st)tau;(sw)tau)]}

158. {H, ((phi)sigma)[1(𝕀)] ⊢ _:Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1)[((∀ (phi)sigma) ∨ psi) |⟶ fiber-point(st;sw)]}

     ∈ 𝕌{[i' | j']}
159. z : {H, ((phi)sigma)[1(𝕀)] ⊢ _:Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1)[((∀ (phi)sigma) ∨ psi)
                                    |⟶ fiber-point(st;sw)]}
160. equiv ((f)sigma)[1(𝕀)] [((∀ (phi)sigma) ∨ psi) ⊢→ (st,  sw)] a'1
= z

∈ {H, ((phi)sigma)[1(𝕀)] ⊢ _:Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1)[((∀ (phi)sigma) ∨ psi) |⟶ fiber-point(st;sw)]}

161. zz : {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

|⟶ fiber-point((st)tau;(sw)tau)]}
162. equiv ((f)sigma o tau+)[1(𝕀)] [((∀ (phi)sigma o tau+) ∨ (psi)tau) ⊢→ (stt, sww)] aa'1
= zz

∈ {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

|⟶ fiber-point((st)tau;(sw)tau)]}

163. (z)tau ∈ {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:(Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1))tau[(((∀ (phi)sigma) ∨ psi))tau

                                              |⟶ (fiber-point(st;sw))tau]}

⊢ H, ((phi)sigma)[1(𝕀)] ⊢ Fiber((equiv-fun((f)sigma))[1(𝕀)];a'1)
BY
{ MemCD }

1
.....subterm..... T:t
1: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)

24. ((equiv-fun(f))sigma)[0(𝕀)] ∈ {H, ((phi)sigma)[0(𝕀)] ⊢ _:(((T)sigma)[0(𝕀)] ⟶ ((A)sigma)[0(𝕀)])}

34. unglue(b0) ∈ {H ⊢ _:((A)sigma)[0(𝕀)][((phi)sigma)[0(𝕀)] |⟶ app(((equiv-fun(f))sigma)[0(𝕀)]; b0)]}

46. unglue(b0) = a0 ∈ {H ⊢ _:((A)sigma)[0(𝕀)][((phi)sigma)[0(𝕀)] |⟶ app(((equiv-fun(f))sigma)[0(𝕀)]; b0)]}

60. comp (cT)sigma [psi ⊢→ b] b0 ∈ {H, (∀ (phi)sigma) ⊢ _:((T)sigma)[1(𝕀)][psi |⟶ (b)[1(𝕀)]]}

73. {K, ((∀ (phi)sigma))tau ⊢ _:(((T)sigma)tau+)[1(𝕀)][(psi)tau |⟶ ((b)tau+)[1(𝕀)]]} ∈ 𝕌{[i | j']}

74. t'1 : {H, (∀ (phi)sigma) ⊢ _:((T)sigma)[1(𝕀)][psi |⟶ (b)[1(𝕀)]]}

75. comp (cT)sigma [psi ⊢→ b] b0 = t'1 ∈ {H, (∀ (phi)sigma) ⊢ _:((T)sigma)[1(𝕀)][psi |⟶ (b)[1(𝕀)]]}

78. (t'1)tau = tt'1 ∈ {K, ((∀ (phi)sigma))tau ⊢ _:(((T)sigma)tau+)[1(𝕀)][(psi)tau |⟶ ((b)tau+)[1(𝕀)]]}

82. pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma) ∈ {H, (∀ (phi)sigma) ⊢ _:((A)sigma)[1(𝕀)]}

∈ {K, ((∀ (phi)sigma))tau ⊢ _:(((A)sigma)tau+)[1(𝕀)][(psi)tau |⟶ app(((equiv-fun(f))sigma)tau+; (b)tau+)[1]]}

85. pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma) ∈ {H, (∀ (phi)sigma) ⊢ _:((A)sigma)[1(𝕀)]}

∈ {K, ((∀ (phi)sigma))tau ⊢ _:(((A)sigma)tau+)[1(𝕀)][(psi)tau |⟶ app(((equiv-fun(f))sigma)tau+; (b)tau+)[1]]}

88. app((equiv-fun(f))sigma; b)[1] ∈ {H, (∀ (phi)sigma), psi ⊢ _:((A)sigma)[1(𝕀)]}

89. {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))[psi

                           |⟶ <>((app((equiv-fun(f))sigma; b)[1])p)]} ∈ 𝕌{[i' | j']}

    ∈ {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))[psi

                                                                   ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                   (b0)tau;((cA)sigma)tau+)

                                    pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

(b0)tau;((cT)sigma)tau+))}
95. ((equiv-fun(f))sigma)tau+ ∈ {K, ((∀ (phi)sigma))tau.𝕀 ⊢ _:(((T)sigma)tau+ ⟶ ((A)sigma)tau+)}

96. app(((equiv-fun(f))sigma)tau+; (b)tau+)[1] ∈ {K, ((∀ (phi)sigma))tau, (psi)tau ⊢ _:(((A)sigma)tau+)[1(𝕀)]}

                                                                     ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                     (b0)tau;((cA)sigma)tau+)

                                      pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

                                              (b0)tau;((cT)sigma)tau+))} ∈ 𝕌{[i' | j']}

                                                                   ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                   (b0)tau;((cA)sigma)tau+)

                                    pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

(b0)tau;((cT)sigma)tau+))}

101. 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))[psi

|⟶ <>((app((equiv-fun(f))sigma; b)[1])p)]}
102. 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))[psi

|⟶ <>((app((equiv-fun(f))sigma; b)[1])p)]}

103. ww : {K, ((∀ (phi)sigma))tau ⊢ _:(Path_(((A)sigma)tau+)[1(𝕀)] pres-c1(K, ((∀ (phi)sigma))tau;(psi)tau;

                                                                           ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                           (b0)tau;((cA)sigma)tau+)

                                            pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

                                                    (b0)tau;((cT)sigma)tau+))}

104. pres (equiv-fun(f))sigma o tau+ [(psi)tau ⊢→ (b)tau+] (b0)tau
= ww
∈ {K, ((∀ (phi)sigma))tau ⊢ _:(Path_(((A)sigma)tau+)[1(𝕀)] pres-c1(K, ((∀ (phi)sigma))tau;(psi)tau;

                                                                   ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                   (b0)tau;((cA)sigma)tau+)

                                    pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

(b0)tau;((cT)sigma)tau+))}
105. (w)tau
= ww
∈ {K, ((∀ (phi)sigma))tau ⊢ _:(Path_(((A)sigma)tau+)[1(𝕀)] pres-c1(K, ((∀ (phi)sigma))tau;(psi)tau;

                                                                   ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                   (b0)tau;((cA)sigma)tau+)

                                    pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

112. (t'1 ∨ (b)[1(𝕀)]) ∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:((T)sigma)[1(𝕀)]}

113. ((t'1 ∨ (b)[1(𝕀)]))tau ∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _:(((T)sigma)[1(𝕀)])tau}

114. (tt'1 ∨ ((b)tau+)[1(𝕀)])
= ((t'1 ∨ (b)[1(𝕀)]))tau
∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _:(((T)sigma)[1(𝕀)])tau}

115. {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _:(((T)sigma)[1(𝕀)])tau} ∈ 𝕌{[i' | j']}

116. st : {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:((T)sigma)[1(𝕀)]}

117. (t'1 ∨ (b)[1(𝕀)]) = st ∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:((T)sigma)[1(𝕀)]}

120. stt = (st)tau ∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _:(((T)sigma)[1(𝕀)])tau}

121. app(equiv-fun(((f)sigma)[1(𝕀)]); st) ∈ {H, ((∀ (phi)sigma) ∨ (((phi)sigma)[1(𝕀)] ∧ psi)) ⊢ _:((A)sigma)[1(𝕀)]}

122. H, ((∀ (phi)sigma) ∨ (((phi)sigma)[1(𝕀)] ∧ psi)) ⊢ (Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))

123. <>((app((equiv-fun(f))sigma; b)[1])p)

     ∈ {H, ((phi)sigma)[1(𝕀)], psi ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))}

124. sub_cubical_set{j:l}(H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi);
H, ((∀ (phi)sigma) ∨ (((phi)sigma)[1(𝕀)] ∧ psi)))

125. H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ (Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))

126. w ∈ {H, ((phi)sigma)[1(𝕀)], (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))

                                                    [psi |⟶ <>((app((equiv-fun(f))sigma; b)[1])p)]}

127. (w ∨ <>((app((equiv-fun(f))sigma; b)[1])p)) ∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _

                                                    :(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))}

128. {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _
:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))} ∈ 𝕌{[i' | j']}

129. ((w ∨ <>((app((equiv-fun(f))sigma; b)[1])p)))tau ∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _

                                                         :((Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]);

                                                                                          st)))tau}

131. sw : {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]);

                                                                                            st))}

132. (w ∨ <>((app((equiv-fun(f))sigma; b)[1])p))
= sw

∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))}

136. equiv-fun(((f)sigma)[1(𝕀)]) ∈ {H, ((phi)sigma)[1(𝕀)] ⊢ _:(((T)sigma)[1(𝕀)] ⟶ ((A)sigma)[1(𝕀)])}

= fiber-comp(K, (((phi)sigma)[1(𝕀)])tau;(((T)sigma)[1(𝕀)])tau;(((A)sigma)[1(𝕀)])tau;(equiv-fun(((f)sigma)[1(𝕀)]))tau;

(a'1)tau;((cT)sigma o [1(𝕀)])tau;((cA)sigma o [1(𝕀)])tau)
∈ K, (((phi)sigma)[1(𝕀)])tau +⊢ Compositon(Fiber((equiv-fun(((f)sigma)[1(𝕀)]))tau;(a'1)tau))

142. K, (((phi)sigma)[1(𝕀)])tau +⊢ Compositon(Fiber((equiv-fun(((f)sigma)[1(𝕀)]))tau;(a'1)tau)) ∈ 𝕌{[i'' | j'']}

             equiv-fun(((f)sigma o tau+)[1(𝕀)]);aa'1;(cT)sigma o tau+ o [1(𝕀)];(cA)sigma o tau+ o [1(𝕀)])

                equiv-fun(((f)sigma o tau+)[1(𝕀)]);aa'1;(cT)sigma o tau+ o [1(𝕀)];(cA)sigma o tau+ o [1(𝕀)])

= cFF
∈ K, (((phi)sigma)[1(𝕀)])tau +⊢ Compositon(Fiber((equiv-fun(((f)sigma)[1(𝕀)]))tau;(a'1)tau))

148. (cF)tau = cFF ∈ K, (((phi)sigma)[1(𝕀)])tau +⊢ Compositon(Fiber((equiv-fun(((f)sigma)[1(𝕀)]))tau;(a'1)tau))

     ∈ {H, ((phi)sigma)[1(𝕀)] ⊢ _:Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1)[((∀ (phi)sigma) ∨ psi) |⟶ fiber-point(st;sw)]}

152. (equiv ((f)sigma)[1(𝕀)] [((∀ (phi)sigma) ∨ psi) ⊢→ (st, sw)] a'1)tau
= equiv (((f)sigma)[1(𝕀)])tau [(((∀ (phi)sigma) ∨ psi))tau ⊢→ ((st)tau, (sw)tau)] (a'1)tau

∈ {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

|⟶ fiber-point((st)tau;(sw)tau)]}

153. fiber-point(st;sw) ∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1)}

                                   :Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)})

156. {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

                                     |⟶ fiber-point((st)tau;(sw)tau)]} ∈ 𝕌{[i' | j']}

157. (equiv ((f)sigma)[1(𝕀)] [((∀ (phi)sigma) ∨ psi) ⊢→ (st, sw)] a'1)tau
= equiv ((f)sigma o tau+)[1(𝕀)] [((∀ (phi)sigma o tau+) ∨ (psi)tau) ⊢→ (stt, sww)] aa'1

∈ {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

|⟶ fiber-point((st)tau;(sw)tau)]}

158. {H, ((phi)sigma)[1(𝕀)] ⊢ _:Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1)[((∀ (phi)sigma) ∨ psi) |⟶ fiber-point(st;sw)]}

∈ {H, ((phi)sigma)[1(𝕀)] ⊢ _:Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1)[((∀ (phi)sigma) ∨ psi) |⟶ fiber-point(st;sw)]}

161. zz : {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

|⟶ fiber-point((st)tau;(sw)tau)]}
162. equiv ((f)sigma o tau+)[1(𝕀)] [((∀ (phi)sigma o tau+) ∨ (psi)tau) ⊢→ (stt, sww)] aa'1
= zz

∈ {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

|⟶ fiber-point((st)tau;(sw)tau)]}

163. (z)tau ∈ {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:(Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1))tau[(((∀ (phi)sigma) ∨ psi))tau

                                              |⟶ (fiber-point(st;sw))tau]}

⊢ H, ((phi)sigma)[1(𝕀)] j⊢

2
.....subterm..... T:t
2: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)

24. ((equiv-fun(f))sigma)[0(𝕀)] ∈ {H, ((phi)sigma)[0(𝕀)] ⊢ _:(((T)sigma)[0(𝕀)] ⟶ ((A)sigma)[0(𝕀)])}

34. unglue(b0) ∈ {H ⊢ _:((A)sigma)[0(𝕀)][((phi)sigma)[0(𝕀)] |⟶ app(((equiv-fun(f))sigma)[0(𝕀)]; b0)]}

46. unglue(b0) = a0 ∈ {H ⊢ _:((A)sigma)[0(𝕀)][((phi)sigma)[0(𝕀)] |⟶ app(((equiv-fun(f))sigma)[0(𝕀)]; b0)]}

60. comp (cT)sigma [psi ⊢→ b] b0 ∈ {H, (∀ (phi)sigma) ⊢ _:((T)sigma)[1(𝕀)][psi |⟶ (b)[1(𝕀)]]}

73. {K, ((∀ (phi)sigma))tau ⊢ _:(((T)sigma)tau+)[1(𝕀)][(psi)tau |⟶ ((b)tau+)[1(𝕀)]]} ∈ 𝕌{[i | j']}

74. t'1 : {H, (∀ (phi)sigma) ⊢ _:((T)sigma)[1(𝕀)][psi |⟶ (b)[1(𝕀)]]}

75. comp (cT)sigma [psi ⊢→ b] b0 = t'1 ∈ {H, (∀ (phi)sigma) ⊢ _:((T)sigma)[1(𝕀)][psi |⟶ (b)[1(𝕀)]]}

78. (t'1)tau = tt'1 ∈ {K, ((∀ (phi)sigma))tau ⊢ _:(((T)sigma)tau+)[1(𝕀)][(psi)tau |⟶ ((b)tau+)[1(𝕀)]]}

82. pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma) ∈ {H, (∀ (phi)sigma) ⊢ _:((A)sigma)[1(𝕀)]}

∈ {K, ((∀ (phi)sigma))tau ⊢ _:(((A)sigma)tau+)[1(𝕀)][(psi)tau |⟶ app(((equiv-fun(f))sigma)tau+; (b)tau+)[1]]}

85. pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma) ∈ {H, (∀ (phi)sigma) ⊢ _:((A)sigma)[1(𝕀)]}

∈ {K, ((∀ (phi)sigma))tau ⊢ _:(((A)sigma)tau+)[1(𝕀)][(psi)tau |⟶ app(((equiv-fun(f))sigma)tau+; (b)tau+)[1]]}

88. app((equiv-fun(f))sigma; b)[1] ∈ {H, (∀ (phi)sigma), psi ⊢ _:((A)sigma)[1(𝕀)]}

89. {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))[psi

                           |⟶ <>((app((equiv-fun(f))sigma; b)[1])p)]} ∈ 𝕌{[i' | j']}

    ∈ {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))[psi

                                                                   ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                   (b0)tau;((cA)sigma)tau+)

                                    pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

(b0)tau;((cT)sigma)tau+))}
95. ((equiv-fun(f))sigma)tau+ ∈ {K, ((∀ (phi)sigma))tau.𝕀 ⊢ _:(((T)sigma)tau+ ⟶ ((A)sigma)tau+)}

96. app(((equiv-fun(f))sigma)tau+; (b)tau+)[1] ∈ {K, ((∀ (phi)sigma))tau, (psi)tau ⊢ _:(((A)sigma)tau+)[1(𝕀)]}

                                                                     ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                     (b0)tau;((cA)sigma)tau+)

                                      pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

                                              (b0)tau;((cT)sigma)tau+))} ∈ 𝕌{[i' | j']}

                                                                   ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                   (b0)tau;((cA)sigma)tau+)

                                    pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

(b0)tau;((cT)sigma)tau+))}

101. 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))[psi

|⟶ <>((app((equiv-fun(f))sigma; b)[1])p)]}
102. 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))[psi

|⟶ <>((app((equiv-fun(f))sigma; b)[1])p)]}

103. ww : {K, ((∀ (phi)sigma))tau ⊢ _:(Path_(((A)sigma)tau+)[1(𝕀)] pres-c1(K, ((∀ (phi)sigma))tau;(psi)tau;

                                                                           ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                           (b0)tau;((cA)sigma)tau+)

                                            pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

                                                    (b0)tau;((cT)sigma)tau+))}

104. pres (equiv-fun(f))sigma o tau+ [(psi)tau ⊢→ (b)tau+] (b0)tau
= ww
∈ {K, ((∀ (phi)sigma))tau ⊢ _:(Path_(((A)sigma)tau+)[1(𝕀)] pres-c1(K, ((∀ (phi)sigma))tau;(psi)tau;

                                                                   ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                   (b0)tau;((cA)sigma)tau+)

                                    pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

(b0)tau;((cT)sigma)tau+))}
105. (w)tau
= ww
∈ {K, ((∀ (phi)sigma))tau ⊢ _:(Path_(((A)sigma)tau+)[1(𝕀)] pres-c1(K, ((∀ (phi)sigma))tau;(psi)tau;

                                                                   ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                   (b0)tau;((cA)sigma)tau+)

                                    pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

112. (t'1 ∨ (b)[1(𝕀)]) ∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:((T)sigma)[1(𝕀)]}

113. ((t'1 ∨ (b)[1(𝕀)]))tau ∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _:(((T)sigma)[1(𝕀)])tau}

114. (tt'1 ∨ ((b)tau+)[1(𝕀)])
= ((t'1 ∨ (b)[1(𝕀)]))tau
∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _:(((T)sigma)[1(𝕀)])tau}

115. {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _:(((T)sigma)[1(𝕀)])tau} ∈ 𝕌{[i' | j']}

116. st : {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:((T)sigma)[1(𝕀)]}

117. (t'1 ∨ (b)[1(𝕀)]) = st ∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:((T)sigma)[1(𝕀)]}

120. stt = (st)tau ∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _:(((T)sigma)[1(𝕀)])tau}

121. app(equiv-fun(((f)sigma)[1(𝕀)]); st) ∈ {H, ((∀ (phi)sigma) ∨ (((phi)sigma)[1(𝕀)] ∧ psi)) ⊢ _:((A)sigma)[1(𝕀)]}

122. H, ((∀ (phi)sigma) ∨ (((phi)sigma)[1(𝕀)] ∧ psi)) ⊢ (Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))

123. <>((app((equiv-fun(f))sigma; b)[1])p)

     ∈ {H, ((phi)sigma)[1(𝕀)], psi ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))}

124. sub_cubical_set{j:l}(H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi);
H, ((∀ (phi)sigma) ∨ (((phi)sigma)[1(𝕀)] ∧ psi)))

125. H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ (Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))

126. w ∈ {H, ((phi)sigma)[1(𝕀)], (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))

                                                    [psi |⟶ <>((app((equiv-fun(f))sigma; b)[1])p)]}

127. (w ∨ <>((app((equiv-fun(f))sigma; b)[1])p)) ∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _

                                                    :(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))}

128. {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _
:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))} ∈ 𝕌{[i' | j']}

129. ((w ∨ <>((app((equiv-fun(f))sigma; b)[1])p)))tau ∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _

                                                         :((Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]);

                                                                                          st)))tau}

131. sw : {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]);

                                                                                            st))}

132. (w ∨ <>((app((equiv-fun(f))sigma; b)[1])p))
= sw

∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))}

136. equiv-fun(((f)sigma)[1(𝕀)]) ∈ {H, ((phi)sigma)[1(𝕀)] ⊢ _:(((T)sigma)[1(𝕀)] ⟶ ((A)sigma)[1(𝕀)])}

= fiber-comp(K, (((phi)sigma)[1(𝕀)])tau;(((T)sigma)[1(𝕀)])tau;(((A)sigma)[1(𝕀)])tau;(equiv-fun(((f)sigma)[1(𝕀)]))tau;

(a'1)tau;((cT)sigma o [1(𝕀)])tau;((cA)sigma o [1(𝕀)])tau)
∈ K, (((phi)sigma)[1(𝕀)])tau +⊢ Compositon(Fiber((equiv-fun(((f)sigma)[1(𝕀)]))tau;(a'1)tau))

142. K, (((phi)sigma)[1(𝕀)])tau +⊢ Compositon(Fiber((equiv-fun(((f)sigma)[1(𝕀)]))tau;(a'1)tau)) ∈ 𝕌{[i'' | j'']}

             equiv-fun(((f)sigma o tau+)[1(𝕀)]);aa'1;(cT)sigma o tau+ o [1(𝕀)];(cA)sigma o tau+ o [1(𝕀)])

                equiv-fun(((f)sigma o tau+)[1(𝕀)]);aa'1;(cT)sigma o tau+ o [1(𝕀)];(cA)sigma o tau+ o [1(𝕀)])

= cFF
∈ K, (((phi)sigma)[1(𝕀)])tau +⊢ Compositon(Fiber((equiv-fun(((f)sigma)[1(𝕀)]))tau;(a'1)tau))

148. (cF)tau = cFF ∈ K, (((phi)sigma)[1(𝕀)])tau +⊢ Compositon(Fiber((equiv-fun(((f)sigma)[1(𝕀)]))tau;(a'1)tau))

     ∈ {H, ((phi)sigma)[1(𝕀)] ⊢ _:Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1)[((∀ (phi)sigma) ∨ psi) |⟶ fiber-point(st;sw)]}

152. (equiv ((f)sigma)[1(𝕀)] [((∀ (phi)sigma) ∨ psi) ⊢→ (st, sw)] a'1)tau
= equiv (((f)sigma)[1(𝕀)])tau [(((∀ (phi)sigma) ∨ psi))tau ⊢→ ((st)tau, (sw)tau)] (a'1)tau

∈ {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

|⟶ fiber-point((st)tau;(sw)tau)]}

153. fiber-point(st;sw) ∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1)}

                                   :Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)})

156. {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

                                     |⟶ fiber-point((st)tau;(sw)tau)]} ∈ 𝕌{[i' | j']}

157. (equiv ((f)sigma)[1(𝕀)] [((∀ (phi)sigma) ∨ psi) ⊢→ (st, sw)] a'1)tau
= equiv ((f)sigma o tau+)[1(𝕀)] [((∀ (phi)sigma o tau+) ∨ (psi)tau) ⊢→ (stt, sww)] aa'1

∈ {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

|⟶ fiber-point((st)tau;(sw)tau)]}

158. {H, ((phi)sigma)[1(𝕀)] ⊢ _:Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1)[((∀ (phi)sigma) ∨ psi) |⟶ fiber-point(st;sw)]}

∈ {H, ((phi)sigma)[1(𝕀)] ⊢ _:Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1)[((∀ (phi)sigma) ∨ psi) |⟶ fiber-point(st;sw)]}

161. zz : {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

|⟶ fiber-point((st)tau;(sw)tau)]}
162. equiv ((f)sigma o tau+)[1(𝕀)] [((∀ (phi)sigma o tau+) ∨ (psi)tau) ⊢→ (stt, sww)] aa'1
= zz

∈ {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

|⟶ fiber-point((st)tau;(sw)tau)]}

163. (z)tau ∈ {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:(Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1))tau[(((∀ (phi)sigma) ∨ psi))tau

                                              |⟶ (fiber-point(st;sw))tau]}

⊢ H, ((phi)sigma)[1(𝕀)] ⊢ ((T)sigma)[1(𝕀)]

3
.....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)

24. ((equiv-fun(f))sigma)[0(𝕀)] ∈ {H, ((phi)sigma)[0(𝕀)] ⊢ _:(((T)sigma)[0(𝕀)] ⟶ ((A)sigma)[0(𝕀)])}

34. unglue(b0) ∈ {H ⊢ _:((A)sigma)[0(𝕀)][((phi)sigma)[0(𝕀)] |⟶ app(((equiv-fun(f))sigma)[0(𝕀)]; b0)]}

46. unglue(b0) = a0 ∈ {H ⊢ _:((A)sigma)[0(𝕀)][((phi)sigma)[0(𝕀)] |⟶ app(((equiv-fun(f))sigma)[0(𝕀)]; b0)]}

60. comp (cT)sigma [psi ⊢→ b] b0 ∈ {H, (∀ (phi)sigma) ⊢ _:((T)sigma)[1(𝕀)][psi |⟶ (b)[1(𝕀)]]}

73. {K, ((∀ (phi)sigma))tau ⊢ _:(((T)sigma)tau+)[1(𝕀)][(psi)tau |⟶ ((b)tau+)[1(𝕀)]]} ∈ 𝕌{[i | j']}

74. t'1 : {H, (∀ (phi)sigma) ⊢ _:((T)sigma)[1(𝕀)][psi |⟶ (b)[1(𝕀)]]}

75. comp (cT)sigma [psi ⊢→ b] b0 = t'1 ∈ {H, (∀ (phi)sigma) ⊢ _:((T)sigma)[1(𝕀)][psi |⟶ (b)[1(𝕀)]]}

78. (t'1)tau = tt'1 ∈ {K, ((∀ (phi)sigma))tau ⊢ _:(((T)sigma)tau+)[1(𝕀)][(psi)tau |⟶ ((b)tau+)[1(𝕀)]]}

82. pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma) ∈ {H, (∀ (phi)sigma) ⊢ _:((A)sigma)[1(𝕀)]}

∈ {K, ((∀ (phi)sigma))tau ⊢ _:(((A)sigma)tau+)[1(𝕀)][(psi)tau |⟶ app(((equiv-fun(f))sigma)tau+; (b)tau+)[1]]}

85. pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma) ∈ {H, (∀ (phi)sigma) ⊢ _:((A)sigma)[1(𝕀)]}

∈ {K, ((∀ (phi)sigma))tau ⊢ _:(((A)sigma)tau+)[1(𝕀)][(psi)tau |⟶ app(((equiv-fun(f))sigma)tau+; (b)tau+)[1]]}

88. app((equiv-fun(f))sigma; b)[1] ∈ {H, (∀ (phi)sigma), psi ⊢ _:((A)sigma)[1(𝕀)]}

89. {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))[psi

                           |⟶ <>((app((equiv-fun(f))sigma; b)[1])p)]} ∈ 𝕌{[i' | j']}

    ∈ {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))[psi

                                                                   ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                   (b0)tau;((cA)sigma)tau+)

                                    pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

(b0)tau;((cT)sigma)tau+))}
95. ((equiv-fun(f))sigma)tau+ ∈ {K, ((∀ (phi)sigma))tau.𝕀 ⊢ _:(((T)sigma)tau+ ⟶ ((A)sigma)tau+)}

96. app(((equiv-fun(f))sigma)tau+; (b)tau+)[1] ∈ {K, ((∀ (phi)sigma))tau, (psi)tau ⊢ _:(((A)sigma)tau+)[1(𝕀)]}

                                                                     ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                     (b0)tau;((cA)sigma)tau+)

                                      pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

                                              (b0)tau;((cT)sigma)tau+))} ∈ 𝕌{[i' | j']}

                                                                   ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                   (b0)tau;((cA)sigma)tau+)

                                    pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

(b0)tau;((cT)sigma)tau+))}

101. 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))[psi

|⟶ <>((app((equiv-fun(f))sigma; b)[1])p)]}
102. 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))[psi

|⟶ <>((app((equiv-fun(f))sigma; b)[1])p)]}

103. ww : {K, ((∀ (phi)sigma))tau ⊢ _:(Path_(((A)sigma)tau+)[1(𝕀)] pres-c1(K, ((∀ (phi)sigma))tau;(psi)tau;

                                                                           ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                           (b0)tau;((cA)sigma)tau+)

                                            pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

                                                    (b0)tau;((cT)sigma)tau+))}

104. pres (equiv-fun(f))sigma o tau+ [(psi)tau ⊢→ (b)tau+] (b0)tau
= ww
∈ {K, ((∀ (phi)sigma))tau ⊢ _:(Path_(((A)sigma)tau+)[1(𝕀)] pres-c1(K, ((∀ (phi)sigma))tau;(psi)tau;

                                                                   ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                   (b0)tau;((cA)sigma)tau+)

                                    pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

(b0)tau;((cT)sigma)tau+))}
105. (w)tau
= ww
∈ {K, ((∀ (phi)sigma))tau ⊢ _:(Path_(((A)sigma)tau+)[1(𝕀)] pres-c1(K, ((∀ (phi)sigma))tau;(psi)tau;

                                                                   ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                   (b0)tau;((cA)sigma)tau+)

                                    pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

112. (t'1 ∨ (b)[1(𝕀)]) ∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:((T)sigma)[1(𝕀)]}

113. ((t'1 ∨ (b)[1(𝕀)]))tau ∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _:(((T)sigma)[1(𝕀)])tau}

114. (tt'1 ∨ ((b)tau+)[1(𝕀)])
= ((t'1 ∨ (b)[1(𝕀)]))tau
∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _:(((T)sigma)[1(𝕀)])tau}

115. {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _:(((T)sigma)[1(𝕀)])tau} ∈ 𝕌{[i' | j']}

116. st : {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:((T)sigma)[1(𝕀)]}

117. (t'1 ∨ (b)[1(𝕀)]) = st ∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:((T)sigma)[1(𝕀)]}

120. stt = (st)tau ∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _:(((T)sigma)[1(𝕀)])tau}

121. app(equiv-fun(((f)sigma)[1(𝕀)]); st) ∈ {H, ((∀ (phi)sigma) ∨ (((phi)sigma)[1(𝕀)] ∧ psi)) ⊢ _:((A)sigma)[1(𝕀)]}

122. H, ((∀ (phi)sigma) ∨ (((phi)sigma)[1(𝕀)] ∧ psi)) ⊢ (Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))

123. <>((app((equiv-fun(f))sigma; b)[1])p)

     ∈ {H, ((phi)sigma)[1(𝕀)], psi ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))}

124. sub_cubical_set{j:l}(H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi);
H, ((∀ (phi)sigma) ∨ (((phi)sigma)[1(𝕀)] ∧ psi)))

125. H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ (Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))

126. w ∈ {H, ((phi)sigma)[1(𝕀)], (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))

                                                    [psi |⟶ <>((app((equiv-fun(f))sigma; b)[1])p)]}

127. (w ∨ <>((app((equiv-fun(f))sigma; b)[1])p)) ∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _

                                                    :(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))}

128. {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _
:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))} ∈ 𝕌{[i' | j']}

129. ((w ∨ <>((app((equiv-fun(f))sigma; b)[1])p)))tau ∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _

                                                         :((Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]);

                                                                                          st)))tau}

131. sw : {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]);

                                                                                            st))}

132. (w ∨ <>((app((equiv-fun(f))sigma; b)[1])p))
= sw

∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))}

136. equiv-fun(((f)sigma)[1(𝕀)]) ∈ {H, ((phi)sigma)[1(𝕀)] ⊢ _:(((T)sigma)[1(𝕀)] ⟶ ((A)sigma)[1(𝕀)])}

= fiber-comp(K, (((phi)sigma)[1(𝕀)])tau;(((T)sigma)[1(𝕀)])tau;(((A)sigma)[1(𝕀)])tau;(equiv-fun(((f)sigma)[1(𝕀)]))tau;

(a'1)tau;((cT)sigma o [1(𝕀)])tau;((cA)sigma o [1(𝕀)])tau)
∈ K, (((phi)sigma)[1(𝕀)])tau +⊢ Compositon(Fiber((equiv-fun(((f)sigma)[1(𝕀)]))tau;(a'1)tau))

142. K, (((phi)sigma)[1(𝕀)])tau +⊢ Compositon(Fiber((equiv-fun(((f)sigma)[1(𝕀)]))tau;(a'1)tau)) ∈ 𝕌{[i'' | j'']}

             equiv-fun(((f)sigma o tau+)[1(𝕀)]);aa'1;(cT)sigma o tau+ o [1(𝕀)];(cA)sigma o tau+ o [1(𝕀)])

                equiv-fun(((f)sigma o tau+)[1(𝕀)]);aa'1;(cT)sigma o tau+ o [1(𝕀)];(cA)sigma o tau+ o [1(𝕀)])

= cFF
∈ K, (((phi)sigma)[1(𝕀)])tau +⊢ Compositon(Fiber((equiv-fun(((f)sigma)[1(𝕀)]))tau;(a'1)tau))

148. (cF)tau = cFF ∈ K, (((phi)sigma)[1(𝕀)])tau +⊢ Compositon(Fiber((equiv-fun(((f)sigma)[1(𝕀)]))tau;(a'1)tau))

     ∈ {H, ((phi)sigma)[1(𝕀)] ⊢ _:Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1)[((∀ (phi)sigma) ∨ psi) |⟶ fiber-point(st;sw)]}

152. (equiv ((f)sigma)[1(𝕀)] [((∀ (phi)sigma) ∨ psi) ⊢→ (st, sw)] a'1)tau
= equiv (((f)sigma)[1(𝕀)])tau [(((∀ (phi)sigma) ∨ psi))tau ⊢→ ((st)tau, (sw)tau)] (a'1)tau

∈ {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

|⟶ fiber-point((st)tau;(sw)tau)]}

153. fiber-point(st;sw) ∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1)}

                                   :Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)})

156. {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

                                     |⟶ fiber-point((st)tau;(sw)tau)]} ∈ 𝕌{[i' | j']}

157. (equiv ((f)sigma)[1(𝕀)] [((∀ (phi)sigma) ∨ psi) ⊢→ (st, sw)] a'1)tau
= equiv ((f)sigma o tau+)[1(𝕀)] [((∀ (phi)sigma o tau+) ∨ (psi)tau) ⊢→ (stt, sww)] aa'1

∈ {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

|⟶ fiber-point((st)tau;(sw)tau)]}

158. {H, ((phi)sigma)[1(𝕀)] ⊢ _:Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1)[((∀ (phi)sigma) ∨ psi) |⟶ fiber-point(st;sw)]}

∈ {H, ((phi)sigma)[1(𝕀)] ⊢ _:Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1)[((∀ (phi)sigma) ∨ psi) |⟶ fiber-point(st;sw)]}

161. zz : {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

|⟶ fiber-point((st)tau;(sw)tau)]}
162. equiv ((f)sigma o tau+)[1(𝕀)] [((∀ (phi)sigma o tau+) ∨ (psi)tau) ⊢→ (stt, sww)] aa'1
= zz

∈ {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

|⟶ fiber-point((st)tau;(sw)tau)]}

163. (z)tau ∈ {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:(Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1))tau[(((∀ (phi)sigma) ∨ psi))tau

                                              |⟶ (fiber-point(st;sw))tau]}

⊢ H, ((phi)sigma)[1(𝕀)] ⊢ ((A)sigma)[1(𝕀)]

4
.....subterm..... T:t
4: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)

24. ((equiv-fun(f))sigma)[0(𝕀)] ∈ {H, ((phi)sigma)[0(𝕀)] ⊢ _:(((T)sigma)[0(𝕀)] ⟶ ((A)sigma)[0(𝕀)])}

34. unglue(b0) ∈ {H ⊢ _:((A)sigma)[0(𝕀)][((phi)sigma)[0(𝕀)] |⟶ app(((equiv-fun(f))sigma)[0(𝕀)]; b0)]}

46. unglue(b0) = a0 ∈ {H ⊢ _:((A)sigma)[0(𝕀)][((phi)sigma)[0(𝕀)] |⟶ app(((equiv-fun(f))sigma)[0(𝕀)]; b0)]}

60. comp (cT)sigma [psi ⊢→ b] b0 ∈ {H, (∀ (phi)sigma) ⊢ _:((T)sigma)[1(𝕀)][psi |⟶ (b)[1(𝕀)]]}

73. {K, ((∀ (phi)sigma))tau ⊢ _:(((T)sigma)tau+)[1(𝕀)][(psi)tau |⟶ ((b)tau+)[1(𝕀)]]} ∈ 𝕌{[i | j']}

74. t'1 : {H, (∀ (phi)sigma) ⊢ _:((T)sigma)[1(𝕀)][psi |⟶ (b)[1(𝕀)]]}

75. comp (cT)sigma [psi ⊢→ b] b0 = t'1 ∈ {H, (∀ (phi)sigma) ⊢ _:((T)sigma)[1(𝕀)][psi |⟶ (b)[1(𝕀)]]}

78. (t'1)tau = tt'1 ∈ {K, ((∀ (phi)sigma))tau ⊢ _:(((T)sigma)tau+)[1(𝕀)][(psi)tau |⟶ ((b)tau+)[1(𝕀)]]}

82. pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma) ∈ {H, (∀ (phi)sigma) ⊢ _:((A)sigma)[1(𝕀)]}

∈ {K, ((∀ (phi)sigma))tau ⊢ _:(((A)sigma)tau+)[1(𝕀)][(psi)tau |⟶ app(((equiv-fun(f))sigma)tau+; (b)tau+)[1]]}

85. pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma) ∈ {H, (∀ (phi)sigma) ⊢ _:((A)sigma)[1(𝕀)]}

∈ {K, ((∀ (phi)sigma))tau ⊢ _:(((A)sigma)tau+)[1(𝕀)][(psi)tau |⟶ app(((equiv-fun(f))sigma)tau+; (b)tau+)[1]]}

88. app((equiv-fun(f))sigma; b)[1] ∈ {H, (∀ (phi)sigma), psi ⊢ _:((A)sigma)[1(𝕀)]}

89. {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))[psi

                           |⟶ <>((app((equiv-fun(f))sigma; b)[1])p)]} ∈ 𝕌{[i' | j']}

    ∈ {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))[psi

                                                                   ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                   (b0)tau;((cA)sigma)tau+)

                                    pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

(b0)tau;((cT)sigma)tau+))}
95. ((equiv-fun(f))sigma)tau+ ∈ {K, ((∀ (phi)sigma))tau.𝕀 ⊢ _:(((T)sigma)tau+ ⟶ ((A)sigma)tau+)}

96. app(((equiv-fun(f))sigma)tau+; (b)tau+)[1] ∈ {K, ((∀ (phi)sigma))tau, (psi)tau ⊢ _:(((A)sigma)tau+)[1(𝕀)]}

                                                                     ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                     (b0)tau;((cA)sigma)tau+)

                                      pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

                                              (b0)tau;((cT)sigma)tau+))} ∈ 𝕌{[i' | j']}

                                                                   ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                   (b0)tau;((cA)sigma)tau+)

                                    pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

(b0)tau;((cT)sigma)tau+))}

101. 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))[psi

|⟶ <>((app((equiv-fun(f))sigma; b)[1])p)]}
102. 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))[psi

|⟶ <>((app((equiv-fun(f))sigma; b)[1])p)]}

103. ww : {K, ((∀ (phi)sigma))tau ⊢ _:(Path_(((A)sigma)tau+)[1(𝕀)] pres-c1(K, ((∀ (phi)sigma))tau;(psi)tau;

                                                                           ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                           (b0)tau;((cA)sigma)tau+)

                                            pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

                                                    (b0)tau;((cT)sigma)tau+))}

104. pres (equiv-fun(f))sigma o tau+ [(psi)tau ⊢→ (b)tau+] (b0)tau
= ww
∈ {K, ((∀ (phi)sigma))tau ⊢ _:(Path_(((A)sigma)tau+)[1(𝕀)] pres-c1(K, ((∀ (phi)sigma))tau;(psi)tau;

                                                                   ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                   (b0)tau;((cA)sigma)tau+)

                                    pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

(b0)tau;((cT)sigma)tau+))}
105. (w)tau
= ww
∈ {K, ((∀ (phi)sigma))tau ⊢ _:(Path_(((A)sigma)tau+)[1(𝕀)] pres-c1(K, ((∀ (phi)sigma))tau;(psi)tau;

                                                                   ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                   (b0)tau;((cA)sigma)tau+)

                                    pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

112. (t'1 ∨ (b)[1(𝕀)]) ∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:((T)sigma)[1(𝕀)]}

113. ((t'1 ∨ (b)[1(𝕀)]))tau ∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _:(((T)sigma)[1(𝕀)])tau}

114. (tt'1 ∨ ((b)tau+)[1(𝕀)])
= ((t'1 ∨ (b)[1(𝕀)]))tau
∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _:(((T)sigma)[1(𝕀)])tau}

115. {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _:(((T)sigma)[1(𝕀)])tau} ∈ 𝕌{[i' | j']}

116. st : {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:((T)sigma)[1(𝕀)]}

117. (t'1 ∨ (b)[1(𝕀)]) = st ∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:((T)sigma)[1(𝕀)]}

120. stt = (st)tau ∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _:(((T)sigma)[1(𝕀)])tau}

121. app(equiv-fun(((f)sigma)[1(𝕀)]); st) ∈ {H, ((∀ (phi)sigma) ∨ (((phi)sigma)[1(𝕀)] ∧ psi)) ⊢ _:((A)sigma)[1(𝕀)]}

122. H, ((∀ (phi)sigma) ∨ (((phi)sigma)[1(𝕀)] ∧ psi)) ⊢ (Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))

123. <>((app((equiv-fun(f))sigma; b)[1])p)

     ∈ {H, ((phi)sigma)[1(𝕀)], psi ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))}

124. sub_cubical_set{j:l}(H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi);
H, ((∀ (phi)sigma) ∨ (((phi)sigma)[1(𝕀)] ∧ psi)))

125. H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ (Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))

126. w ∈ {H, ((phi)sigma)[1(𝕀)], (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))

                                                    [psi |⟶ <>((app((equiv-fun(f))sigma; b)[1])p)]}

127. (w ∨ <>((app((equiv-fun(f))sigma; b)[1])p)) ∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _

                                                    :(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))}

128. {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _
:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))} ∈ 𝕌{[i' | j']}

129. ((w ∨ <>((app((equiv-fun(f))sigma; b)[1])p)))tau ∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _

                                                         :((Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]);

                                                                                          st)))tau}

131. sw : {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]);

                                                                                            st))}

132. (w ∨ <>((app((equiv-fun(f))sigma; b)[1])p))
= sw

∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))}

136. equiv-fun(((f)sigma)[1(𝕀)]) ∈ {H, ((phi)sigma)[1(𝕀)] ⊢ _:(((T)sigma)[1(𝕀)] ⟶ ((A)sigma)[1(𝕀)])}

= fiber-comp(K, (((phi)sigma)[1(𝕀)])tau;(((T)sigma)[1(𝕀)])tau;(((A)sigma)[1(𝕀)])tau;(equiv-fun(((f)sigma)[1(𝕀)]))tau;

(a'1)tau;((cT)sigma o [1(𝕀)])tau;((cA)sigma o [1(𝕀)])tau)
∈ K, (((phi)sigma)[1(𝕀)])tau +⊢ Compositon(Fiber((equiv-fun(((f)sigma)[1(𝕀)]))tau;(a'1)tau))

142. K, (((phi)sigma)[1(𝕀)])tau +⊢ Compositon(Fiber((equiv-fun(((f)sigma)[1(𝕀)]))tau;(a'1)tau)) ∈ 𝕌{[i'' | j'']}

             equiv-fun(((f)sigma o tau+)[1(𝕀)]);aa'1;(cT)sigma o tau+ o [1(𝕀)];(cA)sigma o tau+ o [1(𝕀)])

                equiv-fun(((f)sigma o tau+)[1(𝕀)]);aa'1;(cT)sigma o tau+ o [1(𝕀)];(cA)sigma o tau+ o [1(𝕀)])

= cFF
∈ K, (((phi)sigma)[1(𝕀)])tau +⊢ Compositon(Fiber((equiv-fun(((f)sigma)[1(𝕀)]))tau;(a'1)tau))

148. (cF)tau = cFF ∈ K, (((phi)sigma)[1(𝕀)])tau +⊢ Compositon(Fiber((equiv-fun(((f)sigma)[1(𝕀)]))tau;(a'1)tau))

     ∈ {H, ((phi)sigma)[1(𝕀)] ⊢ _:Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1)[((∀ (phi)sigma) ∨ psi) |⟶ fiber-point(st;sw)]}

152. (equiv ((f)sigma)[1(𝕀)] [((∀ (phi)sigma) ∨ psi) ⊢→ (st, sw)] a'1)tau
= equiv (((f)sigma)[1(𝕀)])tau [(((∀ (phi)sigma) ∨ psi))tau ⊢→ ((st)tau, (sw)tau)] (a'1)tau

∈ {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

|⟶ fiber-point((st)tau;(sw)tau)]}

153. fiber-point(st;sw) ∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1)}

                                   :Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)})

156. {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

                                     |⟶ fiber-point((st)tau;(sw)tau)]} ∈ 𝕌{[i' | j']}

157. (equiv ((f)sigma)[1(𝕀)] [((∀ (phi)sigma) ∨ psi) ⊢→ (st, sw)] a'1)tau
= equiv ((f)sigma o tau+)[1(𝕀)] [((∀ (phi)sigma o tau+) ∨ (psi)tau) ⊢→ (stt, sww)] aa'1

∈ {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

|⟶ fiber-point((st)tau;(sw)tau)]}

158. {H, ((phi)sigma)[1(𝕀)] ⊢ _:Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1)[((∀ (phi)sigma) ∨ psi) |⟶ fiber-point(st;sw)]}

∈ {H, ((phi)sigma)[1(𝕀)] ⊢ _:Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1)[((∀ (phi)sigma) ∨ psi) |⟶ fiber-point(st;sw)]}

161. zz : {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

|⟶ fiber-point((st)tau;(sw)tau)]}
162. equiv ((f)sigma o tau+)[1(𝕀)] [((∀ (phi)sigma o tau+) ∨ (psi)tau) ⊢→ (stt, sww)] aa'1
= zz

∈ {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

|⟶ fiber-point((st)tau;(sw)tau)]}

163. (z)tau ∈ {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:(Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1))tau[(((∀ (phi)sigma) ∨ psi))tau

                                              |⟶ (fiber-point(st;sw))tau]}

⊢ (equiv-fun((f)sigma))[1(𝕀)] ∈ {H, ((phi)sigma)[1(𝕀)] ⊢ _:(((T)sigma)[1(𝕀)] ⟶ ((A)sigma)[1(𝕀)])}

5
.....subterm..... T:t
5: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)

24. ((equiv-fun(f))sigma)[0(𝕀)] ∈ {H, ((phi)sigma)[0(𝕀)] ⊢ _:(((T)sigma)[0(𝕀)] ⟶ ((A)sigma)[0(𝕀)])}

34. unglue(b0) ∈ {H ⊢ _:((A)sigma)[0(𝕀)][((phi)sigma)[0(𝕀)] |⟶ app(((equiv-fun(f))sigma)[0(𝕀)]; b0)]}

46. unglue(b0) = a0 ∈ {H ⊢ _:((A)sigma)[0(𝕀)][((phi)sigma)[0(𝕀)] |⟶ app(((equiv-fun(f))sigma)[0(𝕀)]; b0)]}

60. comp (cT)sigma [psi ⊢→ b] b0 ∈ {H, (∀ (phi)sigma) ⊢ _:((T)sigma)[1(𝕀)][psi |⟶ (b)[1(𝕀)]]}

73. {K, ((∀ (phi)sigma))tau ⊢ _:(((T)sigma)tau+)[1(𝕀)][(psi)tau |⟶ ((b)tau+)[1(𝕀)]]} ∈ 𝕌{[i | j']}

74. t'1 : {H, (∀ (phi)sigma) ⊢ _:((T)sigma)[1(𝕀)][psi |⟶ (b)[1(𝕀)]]}

75. comp (cT)sigma [psi ⊢→ b] b0 = t'1 ∈ {H, (∀ (phi)sigma) ⊢ _:((T)sigma)[1(𝕀)][psi |⟶ (b)[1(𝕀)]]}

78. (t'1)tau = tt'1 ∈ {K, ((∀ (phi)sigma))tau ⊢ _:(((T)sigma)tau+)[1(𝕀)][(psi)tau |⟶ ((b)tau+)[1(𝕀)]]}

82. pres-c1(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma) ∈ {H, (∀ (phi)sigma) ⊢ _:((A)sigma)[1(𝕀)]}

∈ {K, ((∀ (phi)sigma))tau ⊢ _:(((A)sigma)tau+)[1(𝕀)][(psi)tau |⟶ app(((equiv-fun(f))sigma)tau+; (b)tau+)[1]]}

85. pres-c2(H, (∀ (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma) ∈ {H, (∀ (phi)sigma) ⊢ _:((A)sigma)[1(𝕀)]}

∈ {K, ((∀ (phi)sigma))tau ⊢ _:(((A)sigma)tau+)[1(𝕀)][(psi)tau |⟶ app(((equiv-fun(f))sigma)tau+; (b)tau+)[1]]}

88. app((equiv-fun(f))sigma; b)[1] ∈ {H, (∀ (phi)sigma), psi ⊢ _:((A)sigma)[1(𝕀)]}

89. {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))[psi

                           |⟶ <>((app((equiv-fun(f))sigma; b)[1])p)]} ∈ 𝕌{[i' | j']}

    ∈ {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))[psi

                                                                   ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                   (b0)tau;((cA)sigma)tau+)

                                    pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

(b0)tau;((cT)sigma)tau+))}
95. ((equiv-fun(f))sigma)tau+ ∈ {K, ((∀ (phi)sigma))tau.𝕀 ⊢ _:(((T)sigma)tau+ ⟶ ((A)sigma)tau+)}

96. app(((equiv-fun(f))sigma)tau+; (b)tau+)[1] ∈ {K, ((∀ (phi)sigma))tau, (psi)tau ⊢ _:(((A)sigma)tau+)[1(𝕀)]}

                                                                     ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                     (b0)tau;((cA)sigma)tau+)

                                      pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

                                              (b0)tau;((cT)sigma)tau+))} ∈ 𝕌{[i' | j']}

                                                                   ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                   (b0)tau;((cA)sigma)tau+)

                                    pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

(b0)tau;((cT)sigma)tau+))}

101. 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))[psi

|⟶ <>((app((equiv-fun(f))sigma; b)[1])p)]}
102. 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))[psi

|⟶ <>((app((equiv-fun(f))sigma; b)[1])p)]}

103. ww : {K, ((∀ (phi)sigma))tau ⊢ _:(Path_(((A)sigma)tau+)[1(𝕀)] pres-c1(K, ((∀ (phi)sigma))tau;(psi)tau;

                                                                           ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                           (b0)tau;((cA)sigma)tau+)

                                            pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

                                                    (b0)tau;((cT)sigma)tau+))}

104. pres (equiv-fun(f))sigma o tau+ [(psi)tau ⊢→ (b)tau+] (b0)tau
= ww
∈ {K, ((∀ (phi)sigma))tau ⊢ _:(Path_(((A)sigma)tau+)[1(𝕀)] pres-c1(K, ((∀ (phi)sigma))tau;(psi)tau;

                                                                   ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                   (b0)tau;((cA)sigma)tau+)

                                    pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

(b0)tau;((cT)sigma)tau+))}
105. (w)tau
= ww
∈ {K, ((∀ (phi)sigma))tau ⊢ _:(Path_(((A)sigma)tau+)[1(𝕀)] pres-c1(K, ((∀ (phi)sigma))tau;(psi)tau;

                                                                   ((equiv-fun(f))sigma)tau+;(b)tau+;

                                                                   (b0)tau;((cA)sigma)tau+)

                                    pres-c2(K, ((∀ (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;

112. (t'1 ∨ (b)[1(𝕀)]) ∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:((T)sigma)[1(𝕀)]}

113. ((t'1 ∨ (b)[1(𝕀)]))tau ∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _:(((T)sigma)[1(𝕀)])tau}

114. (tt'1 ∨ ((b)tau+)[1(𝕀)])
= ((t'1 ∨ (b)[1(𝕀)]))tau
∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _:(((T)sigma)[1(𝕀)])tau}

115. {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _:(((T)sigma)[1(𝕀)])tau} ∈ 𝕌{[i' | j']}

116. st : {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:((T)sigma)[1(𝕀)]}

117. (t'1 ∨ (b)[1(𝕀)]) = st ∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:((T)sigma)[1(𝕀)]}

120. stt = (st)tau ∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _:(((T)sigma)[1(𝕀)])tau}

121. app(equiv-fun(((f)sigma)[1(𝕀)]); st) ∈ {H, ((∀ (phi)sigma) ∨ (((phi)sigma)[1(𝕀)] ∧ psi)) ⊢ _:((A)sigma)[1(𝕀)]}

122. H, ((∀ (phi)sigma) ∨ (((phi)sigma)[1(𝕀)] ∧ psi)) ⊢ (Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))

123. <>((app((equiv-fun(f))sigma; b)[1])p)

     ∈ {H, ((phi)sigma)[1(𝕀)], psi ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))}

124. sub_cubical_set{j:l}(H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi);
H, ((∀ (phi)sigma) ∨ (((phi)sigma)[1(𝕀)] ∧ psi)))

125. H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ (Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))

126. w ∈ {H, ((phi)sigma)[1(𝕀)], (∀ (phi)sigma) ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))

                                                    [psi |⟶ <>((app((equiv-fun(f))sigma; b)[1])p)]}

127. (w ∨ <>((app((equiv-fun(f))sigma; b)[1])p)) ∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _

                                                    :(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))}

128. {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _
:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))} ∈ 𝕌{[i' | j']}

129. ((w ∨ <>((app((equiv-fun(f))sigma; b)[1])p)))tau ∈ {K, (((phi)sigma)[1(𝕀)])tau, (((∀ (phi)sigma) ∨ psi))tau ⊢ _

                                                         :((Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]);

                                                                                          st)))tau}

131. sw : {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]);

                                                                                            st))}

132. (w ∨ <>((app((equiv-fun(f))sigma; b)[1])p))
= sw

∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:(Path_((A)sigma)[1(𝕀)] a'1 app(equiv-fun(((f)sigma)[1(𝕀)]); st))}

136. equiv-fun(((f)sigma)[1(𝕀)]) ∈ {H, ((phi)sigma)[1(𝕀)] ⊢ _:(((T)sigma)[1(𝕀)] ⟶ ((A)sigma)[1(𝕀)])}

= fiber-comp(K, (((phi)sigma)[1(𝕀)])tau;(((T)sigma)[1(𝕀)])tau;(((A)sigma)[1(𝕀)])tau;(equiv-fun(((f)sigma)[1(𝕀)]))tau;

(a'1)tau;((cT)sigma o [1(𝕀)])tau;((cA)sigma o [1(𝕀)])tau)
∈ K, (((phi)sigma)[1(𝕀)])tau +⊢ Compositon(Fiber((equiv-fun(((f)sigma)[1(𝕀)]))tau;(a'1)tau))

142. K, (((phi)sigma)[1(𝕀)])tau +⊢ Compositon(Fiber((equiv-fun(((f)sigma)[1(𝕀)]))tau;(a'1)tau)) ∈ 𝕌{[i'' | j'']}

             equiv-fun(((f)sigma o tau+)[1(𝕀)]);aa'1;(cT)sigma o tau+ o [1(𝕀)];(cA)sigma o tau+ o [1(𝕀)])

                equiv-fun(((f)sigma o tau+)[1(𝕀)]);aa'1;(cT)sigma o tau+ o [1(𝕀)];(cA)sigma o tau+ o [1(𝕀)])

= cFF
∈ K, (((phi)sigma)[1(𝕀)])tau +⊢ Compositon(Fiber((equiv-fun(((f)sigma)[1(𝕀)]))tau;(a'1)tau))

148. (cF)tau = cFF ∈ K, (((phi)sigma)[1(𝕀)])tau +⊢ Compositon(Fiber((equiv-fun(((f)sigma)[1(𝕀)]))tau;(a'1)tau))

     ∈ {H, ((phi)sigma)[1(𝕀)] ⊢ _:Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1)[((∀ (phi)sigma) ∨ psi) |⟶ fiber-point(st;sw)]}

152. (equiv ((f)sigma)[1(𝕀)] [((∀ (phi)sigma) ∨ psi) ⊢→ (st, sw)] a'1)tau
= equiv (((f)sigma)[1(𝕀)])tau [(((∀ (phi)sigma) ∨ psi))tau ⊢→ ((st)tau, (sw)tau)] (a'1)tau

∈ {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

|⟶ fiber-point((st)tau;(sw)tau)]}

153. fiber-point(st;sw) ∈ {H, ((phi)sigma)[1(𝕀)], ((∀ (phi)sigma) ∨ psi) ⊢ _:Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1)}

                                   :Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)})

156. {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

                                     |⟶ fiber-point((st)tau;(sw)tau)]} ∈ 𝕌{[i' | j']}

157. (equiv ((f)sigma)[1(𝕀)] [((∀ (phi)sigma) ∨ psi) ⊢→ (st, sw)] a'1)tau
= equiv ((f)sigma o tau+)[1(𝕀)] [((∀ (phi)sigma o tau+) ∨ (psi)tau) ⊢→ (stt, sww)] aa'1

∈ {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

|⟶ fiber-point((st)tau;(sw)tau)]}

158. {H, ((phi)sigma)[1(𝕀)] ⊢ _:Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1)[((∀ (phi)sigma) ∨ psi) |⟶ fiber-point(st;sw)]}

∈ {H, ((phi)sigma)[1(𝕀)] ⊢ _:Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1)[((∀ (phi)sigma) ∨ psi) |⟶ fiber-point(st;sw)]}

161. zz : {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

|⟶ fiber-point((st)tau;(sw)tau)]}
162. equiv ((f)sigma o tau+)[1(𝕀)] [((∀ (phi)sigma o tau+) ∨ (psi)tau) ⊢→ (stt, sww)] aa'1
= zz

∈ {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:Fiber(equiv-fun((((f)sigma)[1(𝕀)])tau);(a'1)tau)[(((∀ (phi)sigma) ∨ psi))tau

|⟶ fiber-point((st)tau;(sw)tau)]}

163. (z)tau ∈ {K, (((phi)sigma)[1(𝕀)])tau ⊢ _:(Fiber(equiv-fun(((f)sigma)[1(𝕀)]);a'1))tau[(((∀ (phi)sigma) ∨ psi))tau

                                              |⟶ (fiber-point(st;sw))tau]}

⊢ a'1 ∈ {H, ((phi)sigma)[1(𝕀)] ⊢ _:((A)sigma)[1(𝕀)]}

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 : 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{})][psi |{}\mrightarrow{} (b)[0(\mBbbI{})]]\} 16. G \mvdash{} Glue [phi \mvdash{}\mrightarrow{} (T;equiv-fun(f))] A 17. (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 18. b \mmember{} \{H.\mBbbI{}, (psi)p \mvdash{} \_:Glue [(phi)sigma \mvdash{}\mrightarrow{} ((T)sigma;(equiv-fun(f))sigma)] (A)sigma\} 19. (phi)sigma \mmember{} \{H.\mBbbI{} \mvdash{} \_:\mBbbF{}\} 20. (equiv-fun(f))sigma \mmember{} \{H.\mBbbI{}, (phi)sigma \mvdash{} \_:((T)sigma {}\mrightarrow{} (A)sigma)\} 21. \{H.\mBbbI{}, (phi)sigma \mvdash{} \_\} \msubseteq{}r \{H.\mBbbI{}, (psi)p, (phi)sigma \mvdash{} \_\} 22. H, ((phi)sigma)[0(\mBbbI{})] \mvdash{} ((T)sigma)[0(\mBbbI{})] 23. ((equiv-fun(f))sigma)[0(\mBbbI{})] \mmember{} \{H, ((phi)sigma)[0(\mBbbI{})] \mvdash{} \_:(((T {}\mrightarrow{} A))sigma)[0(\mBbbI{})]\} 24. ((equiv-fun(f))sigma)[0(\mBbbI{})] \mmember{} \{H, ((phi)sigma)[0(\mBbbI{})] \mvdash{} \_:(((T)sigma)[0(\mBbbI{})] {}\mrightarrow{} ((A)sigma)[0(\mBbbI{})])\} 25. sub\_cubical\_set\{j:l\}(H, (\mforall{} (phi)sigma), psi.\mBbbI{}; H.\mBbbI{}, (psi)p, (phi)sigma) 26. H, (\mforall{} (phi)sigma).\mBbbI{} \mvdash{} (T)sigma 27. H.\mBbbI{}, (phi)sigma +\mvdash{} Compositon((T)sigma) \msubseteq{}r H, (\mforall{} (phi)sigma).\mBbbI{} +\mvdash{} Compositon((T)sigma) 28. H.\mBbbI{}, (phi)sigma +\mvdash{} Compositon((A)sigma) \msubseteq{}r H, (\mforall{} (phi)sigma).\mBbbI{} +\mvdash{} Compositon((A)sigma) 29. H.\mBbbI{}, (psi)p, (phi)sigma \mvdash{} (T)sigma 30. H, (\mforall{} (phi)sigma) \mvdash{} ((T)sigma)[1(\mBbbI{})] 31. \{H, ((phi)sigma)[1(\mBbbI{})] \mvdash{} \_\} \msubseteq{}r \{H, (\mforall{} (phi)sigma) \mvdash{} \_\} 32. H, (\mforall{} (phi)sigma) \mvdash{} ((T)sigma)[1(\mBbbI{})] 33. unglue(b) \mmember{} \{H.\mBbbI{}, (psi)p \mvdash{} \_:(A)sigma[(phi)sigma |{}\mrightarrow{} app((equiv-fun(f))sigma; b)]\} 34. unglue(b0) \mmember{} \{H \mvdash{} \_:((A)sigma)[0(\mBbbI{})][((phi)sigma)[0(\mBbbI{})] |{}\mrightarrow{} app(((equiv-fun(f))sigma)[0(\mBbbI{})]; b0)]\} 35. (cT)sigma \mmember{} H, (\mforall{} (phi)sigma).\mBbbI{} +\mvdash{} Compositon((T)sigma) 36. (cA)sigma \mmember{} H, (\mforall{} (phi)sigma).\mBbbI{} +\mvdash{} Compositon((A)sigma) 37. b0 \mmember{} \{H, ((phi)sigma)[0(\mBbbI{})] \mvdash{} \_:((T)sigma)[0(\mBbbI{})]\} 38. b \mmember{} \{H.\mBbbI{}, (psi)p, (phi)sigma \mvdash{} \_:(T)sigma\} 39. app((equiv-fun(f))sigma; b) \mmember{} \{H.\mBbbI{}, (psi)p, (phi)sigma \mvdash{} \_:(A)sigma\} 40. H, ((phi)sigma)[1(\mBbbI{})] \mvdash{} ((T)sigma)[1(\mBbbI{})] 41. \{H, ((phi)sigma)[1(\mBbbI{})] \mvdash{} \_\} \msubseteq{}r \{H, (\mforall{} (phi)sigma) \mvdash{} \_\} 42. H, (\mforall{} (phi)sigma) \mvdash{} ((T)sigma)[1(\mBbbI{})] 43. a : \{H.\mBbbI{}, (psi)p \mvdash{} \_:(A)sigma[(phi)sigma |{}\mrightarrow{} app((equiv-fun(f))sigma; b)]\} 44. unglue(b) = a 45. a0 : \{H \mvdash{} \_:((A)sigma)[0(\mBbbI{})][((phi)sigma)[0(\mBbbI{})] |{}\mrightarrow{} app(((equiv-fun(f))sigma)[0(\mBbbI{})]; b0)]\} 46. unglue(b0) = a0 47. a0 \mmember{} \{H \mvdash{} \_:((A)sigma)[0(\mBbbI{})][psi |{}\mrightarrow{} a[0]]\} 48. (comp (cA)sigma [psi \mvdash{}\mrightarrow{} a] a0)tau = comp ((cA)sigma)tau+ [(psi)tau \mvdash{}\mrightarrow{} (a)tau+] (a0)tau 49. comp (cA)sigma [psi \mvdash{}\mrightarrow{} a] a0 \mmember{} \{H \mvdash{} \_:((A)sigma)[1(\mBbbI{})][psi |{}\mrightarrow{} a[1]]\} 50. a'1 : \{H \mvdash{} \_:((A)sigma)[1(\mBbbI{})][psi |{}\mrightarrow{} a[1]]\} 51. comp (cA)sigma [psi \mvdash{}\mrightarrow{} a] a0 = a'1 52. ((psi)p)tau+ \mmember{} \{K.\mBbbI{} \mvdash{} \_:\mBbbF{}\} 53. \{K \mvdash{} \_:(((A)sigma)tau+)[1(\mBbbI{})][(psi)tau |{}\mrightarrow{} ((a)tau+)[1(\mBbbI{})]]\} \mmember{} \mBbbU{}\{[i' | j']\} 54. aa'1 : \{K \mvdash{} \_:(((A)sigma)tau+)[1(\mBbbI{})][(psi)tau |{}\mrightarrow{} ((a)tau+)[1(\mBbbI{})]]\} 55. comp ((cA)sigma)tau+ [(psi)tau \mvdash{}\mrightarrow{} (a)tau+] (a0)tau = aa'1 56. (a'1)tau = aa'1 57. b \mmember{} \{H, (\mforall{} (phi)sigma), psi.\mBbbI{} \mvdash{} \_:(T)sigma\} 58. (b)[0(\mBbbI{})] = b0 59. b0 \mmember{} \{H, (\mforall{} (phi)sigma) \mvdash{} \_:((T)sigma)[0(\mBbbI{})][psi |{}\mrightarrow{} (b)[0(\mBbbI{})]]\} 60. comp (cT)sigma [psi \mvdash{}\mrightarrow{} b] b0 \mmember{} \{H, (\mforall{} (phi)sigma) \mvdash{} \_:((T)sigma)[1(\mBbbI{})][psi |{}\mrightarrow{} (b)[1(\mBbbI{})]]\} 61. (comp (cT)sigma [psi \mvdash{}\mrightarrow{} b] b0)tau = comp ((cT)sigma)tau+ [(psi)tau \mvdash{}\mrightarrow{} (b)tau+] (b0)tau 62. H, ((phi)sigma)[1(\mBbbI{})] \mvdash{} ((T)sigma)[1(\mBbbI{})] 63. (b)[1(\mBbbI{})] \mmember{} \{H, ((phi)sigma)[1(\mBbbI{})], psi \mvdash{} \_:((T)sigma)[1(\mBbbI{})]\} 64. \{H, ((phi)sigma)[1(\mBbbI{})] \mvdash{} \_\} \msubseteq{}r \{H, (\mforall{} (phi)sigma) \mvdash{} \_\} 65. H, (\mforall{} (phi)sigma) \mvdash{} ((T)sigma)[1(\mBbbI{})] 66. (b)[1(\mBbbI{})] \mmember{} \{H, (\mforall{} (phi)sigma), psi \mvdash{} \_:((T)sigma)[1(\mBbbI{})]\} 67. \{H, (\mforall{} (phi)sigma) \mvdash{} \_:((T)sigma)[1(\mBbbI{})][psi |{}\mrightarrow{} (b)[1(\mBbbI{})]]\} \mmember{} \mBbbU{}\{[i' | j']\} 68. sub\_cubical\_set\{j:l\}(K, ((\mforall{} (phi)sigma))tau.\mBbbI{}; K.\mBbbI{}, (phi)sigma o tau+) 69. sub\_cubical\_set\{j:l\}(K, ((\mforall{} (phi)sigma))tau.\mBbbI{}; K.\mBbbI{}, ((phi)sigma)tau+) 70. \{K.\mBbbI{}, ((phi)sigma)tau+ \mvdash{} \_\} \msubseteq{}r \{K, ((\mforall{} (phi)sigma))tau.\mBbbI{} \mvdash{} \_\} 71. K, ((\mforall{} (phi)sigma))tau.\mBbbI{} \mvdash{} ((T)sigma)tau+ 72. (comp (cT)sigma [psi \mvdash{}\mrightarrow{} b] b0)tau = comp (cT)sigma o tau+ [(psi)tau \mvdash{}\mrightarrow{} (b)tau+] (b0)tau 73. \{K, ((\mforall{} (phi)sigma))tau \mvdash{} \_:(((T)sigma)tau+)[1(\mBbbI{})][(psi)tau |{}\mrightarrow{} ((b)tau+)[1(\mBbbI{})]]\} \mmember{} \mBbbU{}\{[i | j']\} 74. t'1 : \{H, (\mforall{} (phi)sigma) \mvdash{} \_:((T)sigma)[1(\mBbbI{})][psi |{}\mrightarrow{} (b)[1(\mBbbI{})]]\} 75. comp (cT)sigma [psi \mvdash{}\mrightarrow{} b] b0 = t'1 76. tt'1 : \{K, ((\mforall{} (phi)sigma))tau \mvdash{} \_:(((T)sigma)tau+)[1(\mBbbI{})][(psi)tau |{}\mrightarrow{} ((b)tau+)[1(\mBbbI{})]]\} 77. comp (cT)sigma o tau+ [(psi)tau \mvdash{}\mrightarrow{} (b)tau+] (b0)tau = tt'1 78. (t'1)tau = tt'1 79. (equiv-fun(f))sigma \mmember{} \{H, (\mforall{} (phi)sigma).\mBbbI{} \mvdash{} \_:((T)sigma {}\mrightarrow{} (A)sigma)\} 80. b \mmember{} \{H, (\mforall{} (phi)sigma).\mBbbI{}, (psi)p \mvdash{} \_:(T)sigma\} 81. b0 \mmember{} \{H, (\mforall{} (phi)sigma) \mvdash{} \_:((T)sigma)[0(\mBbbI{})][psi |{}\mrightarrow{} b[0]]\} 82. 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{})]\} 83. partial-term-1(H, (\mforall{} (phi)sigma);app((equiv-fun(f))sigma; b)) = pres-c1(H, (\mforall{} (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma) 84. (pres-c1(H, (\mforall{} (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cA)sigma))tau = pres-c1(K, ((\mforall{} (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;(b0)tau;((cA)sigma)tau+) 85. 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{})]\} 86. partial-term-1(H, (\mforall{} (phi)sigma);app((equiv-fun(f))sigma; b)) = pres-c2(H, (\mforall{} (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma) 87. (pres-c2(H, (\mforall{} (phi)sigma);psi;(equiv-fun(f))sigma;b;b0;(cT)sigma))tau = pres-c2(K, ((\mforall{} (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+;(b0)tau;((cT)sigma)tau+) 88. app((equiv-fun(f))sigma; b)[1] \mmember{} \{H, (\mforall{} (phi)sigma), psi \mvdash{} \_:((A)sigma)[1(\mBbbI{})]\} 89. \{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)) [psi |{}\mrightarrow{} <>((app((equiv-fun(f))sigma; b)[1])p)]\} \mmember{} \mBbbU{}\{[i' | j']\} 90. (equiv-fun(f))sigma \mmember{} \{H, (\mforall{} (phi)sigma).\mBbbI{} \mvdash{} \_:((T)sigma {}\mrightarrow{} (A)sigma)\} 91. b \mmember{} \{H, (\mforall{} (phi)sigma).\mBbbI{}, (psi)p \mvdash{} \_:(T)sigma\} 92. b0 \mmember{} \{H, (\mforall{} (phi)sigma) \mvdash{} \_:((T)sigma)[0(\mBbbI{})][psi |{}\mrightarrow{} b[0]]\} 93. 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))[psi |{}\mrightarrow{} <>((app((equiv-fun(f))sigma; b)[1])p)]\} 94. (pres (equiv-fun(f))sigma [psi \mvdash{}\mrightarrow{} b] b0)tau = pres ((equiv-fun(f))sigma)tau+ [(psi)tau \mvdash{}\mrightarrow{} (b)tau+] (b0)tau 95. ((equiv-fun(f))sigma)tau+ \mmember{} \{K, ((\mforall{} (phi)sigma))tau.\mBbbI{} \mvdash{} \_:(((T)sigma)tau+ {}\mrightarrow{} ((A)sigma)tau+)\} 96. app(((equiv-fun(f))sigma)tau+; (b)tau+)[1] \mmember{} \{K, ((\mforall{} (phi)sigma))tau, (psi)tau \mvdash{} \_:(((A)sigma)tau+)[1(\mBbbI{})]\} 97. pres-c1(K, ((\mforall{} (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+; (b0)tau;((cA)sigma)tau+) \mmember{} \{K, ((\mforall{} (phi)sigma))tau \mvdash{} \_:(((A)sigma)tau+)[1(\mBbbI{})]\} 98. pres-c2(K, ((\mforall{} (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+; (b0)tau;((cT)sigma)tau+) \mmember{} \{K, ((\mforall{} (phi)sigma))tau \mvdash{} \_:(((A)sigma)tau+)[1(\mBbbI{})]\} 99. \{K, ((\mforall{} (phi)sigma))tau \mvdash{} \_ :(Path\_(((A)sigma)tau+)[1(\mBbbI{})] pres-c1(K, ((\mforall{} (phi)sigma))tau;(psi)tau; ((equiv-fun(f))sigma)tau+;(b)tau+; (b0)tau;((cA)sigma)tau+) pres-c2(K, ((\mforall{} (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+; (b0)tau;((cT)sigma)tau+))\} \mmember{} \mBbbU{}\{[i' | j']\} 100. (pres (equiv-fun(f))sigma [psi \mvdash{}\mrightarrow{} b] b0)tau = pres (equiv-fun(f))sigma o tau+ [(psi)tau \mvdash{}\mrightarrow{} (b)tau+] (b0)tau 101. 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))[psi |{}\mrightarrow{} <>((app((equiv-fun(f))sigma; b)[1])p)]\} 102. pres (equiv-fun(f))sigma [psi \mvdash{}\mrightarrow{} b] b0 = w 103. ww : \{K, ((\mforall{} (phi)sigma))tau \mvdash{} \_ :(Path\_(((A)sigma)tau+)[1(\mBbbI{})] pres-c1(K, ((\mforall{} (phi)sigma))tau;(psi)tau; ((equiv-fun(f))sigma)tau+;(b)tau+; (b0)tau;((cA)sigma)tau+) pres-c2(K, ((\mforall{} (phi)sigma))tau;(psi)tau;((equiv-fun(f))sigma)tau+;(b)tau+; (b0)tau;((cT)sigma)tau+))\} 104. pres (equiv-fun(f))sigma o tau+ [(psi)tau \mvdash{}\mrightarrow{} (b)tau+] (b0)tau = ww 105. (w)tau = ww 106. H, ((phi)sigma)[1(\mBbbI{})] \mvdash{} ((T)sigma)[1(\mBbbI{})] 107. (b)[1(\mBbbI{})] \mmember{} \{H, ((phi)sigma)[1(\mBbbI{})], psi \mvdash{} \_:((T)sigma)[1(\mBbbI{})]\} 108. H, (\mforall{} (phi)sigma) \mvdash{} ((T)sigma)[1(\mBbbI{})] 109. (b)[1(\mBbbI{})] \mmember{} \{H, (\mforall{} (phi)sigma), psi \mvdash{} \_:((T)sigma)[1(\mBbbI{})]\} 110. \{H, (\mforall{} (phi)sigma) \mvdash{} \_:((T)sigma)[1(\mBbbI{})][psi |{}\mrightarrow{} (b)[1(\mBbbI{})]]\} \msubseteq{}r \{H, ((phi)sigma)[1(\mBbbI{})], (\mforall{} (phi)sigma) \mvdash{} \_:((T)sigma)[1(\mBbbI{})][psi |{}\mrightarrow{} (b)[1(\mBbbI{})]]\} 111. H, ((phi)sigma)[1(\mBbbI{})], ((\mforall{} (phi)sigma) \mvee{} psi) \mvdash{} ((T)sigma)[1(\mBbbI{})] 112. (t'1 \mvee{} (b)[1(\mBbbI{})]) \mmember{} \{H, ((phi)sigma)[1(\mBbbI{})], ((\mforall{} (phi)sigma) \mvee{} psi) \mvdash{} \_:((T)sigma)[1(\mBbbI{})]\} 113. ((t'1 \mvee{} (b)[1(\mBbbI{})]))tau \mmember{} \{K, (((phi)sigma)[1(\mBbbI{})])tau, (((\mforall{} (phi)sigma) \mvee{} psi))tau \mvdash{} \_ :(((T)sigma)[1(\mBbbI{})])tau\} 114. (tt'1 \mvee{} ((b)tau+)[1(\mBbbI{})]) = ((t'1 \mvee{} (b)[1(\mBbbI{})]))tau 115. \{K, (((phi)sigma)[1(\mBbbI{})])tau, (((\mforall{} (phi)sigma) \mvee{} psi))tau \mvdash{} \_:(((T)sigma)[1(\mBbbI{})])tau\} \mmember{} \mBbbU{}\{[i' | j']\} 116. st : \{H, ((phi)sigma)[1(\mBbbI{})], ((\mforall{} (phi)sigma) \mvee{} psi) \mvdash{} \_:((T)sigma)[1(\mBbbI{})]\} 117. (t'1 \mvee{} (b)[1(\mBbbI{})]) = st 118. stt : \{K, (((phi)sigma)[1(\mBbbI{})])tau, (((\mforall{} (phi)sigma) \mvee{} psi))tau \mvdash{} \_:(((T)sigma)[1(\mBbbI{})])tau\} 119. (tt'1 \mvee{} ((b)tau+)[1(\mBbbI{})]) = stt 120. stt = (st)tau 121. app(equiv-fun(((f)sigma)[1(\mBbbI{})]); st) \mmember{} \{H, ((\mforall{} (phi)sigma) \mvee{} (((phi)sigma)[1(\mBbbI{})] \mwedge{} psi)) \mvdash{} \_ :((A)sigma)[1(\mBbbI{})]\} 122. H, ((\mforall{} (phi)sigma) \mvee{} (((phi)sigma)[1(\mBbbI{})] \mwedge{} psi)) \mvdash{} (Path\_((A)sigma)[1(\mBbbI{})] a'1 app(equiv-fun(((f)sigma)[1(\mBbbI{})]); st)) 123. <>((app((equiv-fun(f))sigma; b)[1])p) \mmember{} \{H, ((phi)sigma)[1(\mBbbI{})], psi \mvdash{} \_ :(Path\_((A)sigma)[1(\mBbbI{})] a'1 app(equiv-fun(((f)sigma)[1(\mBbbI{})]); st))\} 124. sub\_cubical\_set\{j:l\}(H, ((phi)sigma)[1(\mBbbI{})], ((\mforall{} (phi)sigma) \mvee{} psi); H, ((\mforall{} (phi)sigma) \mvee{} (((phi)sigma)[1(\mBbbI{})] \mwedge{} psi))) 125. H, ((phi)sigma)[1(\mBbbI{})], ((\mforall{} (phi)sigma) \mvee{} psi) \mvdash{} (Path\_((A)sigma)[1(\mBbbI{})] a'1 app(equiv-fun(((f)sigma)[1(\mBbbI{})]); st)) 126. w \mmember{} \{H, ((phi)sigma)[1(\mBbbI{})], (\mforall{} (phi)sigma) \mvdash{} \_:(Path\_((A)sigma)[1(\mBbbI{})] a'1 app(equiv-fun(((f)sigma)[1(\mBbbI{})]); st))[psi |{}\mrightarrow{} <>((app((equiv-fun(f))sigma; b)[1])p)]\} 127. (w \mvee{} <>((app((equiv-fun(f))sigma; b)[1])p)) \mmember{} \{H, ((phi)sigma)[1(\mBbbI{})], ((\mforall{} (phi)sigma) \mvee{} psi) \mvdash{} \_ :(Path\_((A)sigma)[1(\mBbbI{})] a'1 app(equiv-fun(((f)sigma)[1(\mBbbI{})]); st))\} 128. \{H, ((phi)sigma)[1(\mBbbI{})], ((\mforall{} (phi)sigma) \mvee{} psi) \mvdash{} \_ :(Path\_((A)sigma)[1(\mBbbI{})] a'1 app(equiv-fun(((f)sigma)[1(\mBbbI{})]); st))\} \mmember{} \mBbbU{}\{[i' | j']\} 129. ((w \mvee{} <>((app((equiv-fun(f))sigma; b)[1])p)))tau \mmember{} \{K, (((phi)sigma)[1(\mBbbI{})])tau, (((\mforall{} (phi)sigma) \mvee{} psi))tau \mvdash{} \_ :((Path\_((A)sigma)[1(\mBbbI{})] a'1 app(equiv-fun(((f)sigma)[1(\mBbbI{})]); st)))tau\} 130. ((w \mvee{} <>((app((equiv-fun(f))sigma; b)[1])p)))tau = (ww \mvee{} <>((app((equiv-fun(f))sigma o tau+; (b)tau+)[1])p)) 131. sw : \{H, ((phi)sigma)[1(\mBbbI{})], ((\mforall{} (phi)sigma) \mvee{} psi) \mvdash{} \_ :(Path\_((A)sigma)[1(\mBbbI{})] a'1 app(equiv-fun(((f)sigma)[1(\mBbbI{})]); st))\} 132. (w \mvee{} <>((app((equiv-fun(f))sigma; b)[1])p)) = sw 133. sww : \{K, (((phi)sigma)[1(\mBbbI{})])tau, (((\mforall{} (phi)sigma) \mvee{} psi))tau \mvdash{} \_ :((Path\_((A)sigma)[1(\mBbbI{})] a'1 app(equiv-fun(((f)sigma)[1(\mBbbI{})]); st)))tau\} 134. (ww \mvee{} <>((app((equiv-fun(f))sigma o tau+; (b)tau+)[1])p)) = sww 135. (sw)tau = sww 136. equiv-fun(((f)sigma)[1(\mBbbI{})]) \mmember{} \{H, ((phi)sigma)[1(\mBbbI{})] \mvdash{} \_:(((T)sigma)[1(\mBbbI{})] {}\mrightarrow{} ((A)sigma)[1(\mBbbI{})])\} 137. 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{})]) \mmember{} H, ((phi)sigma)[1(\mBbbI{})] +\mvdash{} Compositon(Fiber(equiv-fun(((f)sigma)[1(\mBbbI{})]);a'1)) 138. H, ((phi)sigma)[1(\mBbbI{})] +\mvdash{} Compositon(Fiber(equiv-fun(((f)sigma)[1(\mBbbI{})]);a'1)) \mmember{} \mBbbU{}\{[i'' | j'']\} 139. a'1 \mmember{} \{H, ((phi)sigma)[1(\mBbbI{})] \mvdash{} \_:((A)sigma)[1(\mBbbI{})]\} 140. ((cA)sigma o [1(\mBbbI{})] \mmember{} H, ((phi)sigma)[1(\mBbbI{})] +\mvdash{} Compositon(((A)sigma)[1(\mBbbI{})])) \mwedge{} ((cT)sigma o [1(\mBbbI{})] \mmember{} H, ((phi)sigma)[1(\mBbbI{})] +\mvdash{} Compositon(((T)sigma)[1(\mBbbI{})])) 141. (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{})]))tau = fiber-comp(K, (((phi)sigma)[1(\mBbbI{})])tau;(((T)sigma)[1(\mBbbI{})])tau;(((A)sigma)[1(\mBbbI{})])tau; (equiv-fun(((f)sigma)[1(\mBbbI{})]))tau;(a'1)tau;((cT)sigma o [1(\mBbbI{})])tau; ((cA)sigma o [1(\mBbbI{})])tau) 142. K, (((phi)sigma)[1(\mBbbI{})])tau +\mvdash{} Compositon(Fiber((equiv-fun(((f)sigma)[1(\mBbbI{})]))tau;(a'1)tau)) \mmember{} \mBbbU{}\{[i'' | j'']\} 143. (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{})]))tau = fiber-comp(K, ((phi)sigma o tau+)[1(\mBbbI{})];((T)sigma o tau+)[1(\mBbbI{})];((A)sigma o tau+)[1(\mBbbI{})]; equiv-fun(((f)sigma o tau+)[1(\mBbbI{})]);aa'1;(cT)sigma o tau+ o [1(\mBbbI{})]; (cA)sigma o tau+ o [1(\mBbbI{})]) 144. cF : H, ((phi)sigma)[1(\mBbbI{})] +\mvdash{} Compositon(Fiber(equiv-fun(((f)sigma)[1(\mBbbI{})]);a'1)) 145. 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 146. cFF : K, (((phi)sigma)[1(\mBbbI{})])tau +\mvdash{} Compositon(Fiber((equiv-fun(((f)sigma)[1(\mBbbI{})]))tau; (a'1)tau)) 147. fiber-comp(K, ((phi)sigma o tau+)[1(\mBbbI{})];((T)sigma o tau+)[1(\mBbbI{})];((A)sigma o tau+)[1(\mBbbI{})]; equiv-fun(((f)sigma o tau+)[1(\mBbbI{})]);aa'1;(cT)sigma o tau+ o [1(\mBbbI{})]; (cA)sigma o tau+ o [1(\mBbbI{})]) = cFF 148. (cF)tau = cFF 149. a'1 \mmember{} \{H, ((phi)sigma)[1(\mBbbI{})] \mvdash{} \_:((A)sigma)[1(\mBbbI{})]\} 150. ((f)sigma)[1(\mBbbI{})] \mmember{} \{H, ((phi)sigma)[1(\mBbbI{})] \mvdash{} \_:Equiv(((T)sigma)[1(\mBbbI{})];((A)sigma)[1(\mBbbI{})])\} 151. equiv ((f)sigma)[1(\mBbbI{})] [((\mforall{} (phi)sigma) \mvee{} psi) \mvdash{}\mrightarrow{} (st, sw)] a'1 \mmember{} \{H, ((phi)sigma)[1(\mBbbI{})] \mvdash{} \_:Fiber(equiv-fun(((f)sigma)[1(\mBbbI{})]);a'1)[((\mforall{} (phi)sigma) \mvee{} psi) |{}\mrightarrow{} fiber-point(st;sw)]\} 152. (equiv ((f)sigma)[1(\mBbbI{})] [((\mforall{} (phi)sigma) \mvee{} psi) \mvdash{}\mrightarrow{} (st, sw)] a'1)tau = equiv (((f)sigma)[1(\mBbbI{})])tau [(((\mforall{} (phi)sigma) \mvee{} psi))tau \mvdash{}\mrightarrow{} ((st)tau, (sw)tau)] (a'1)tau 153. fiber-point(st;sw) \mmember{} \{H, ((phi)sigma)[1(\mBbbI{})], ((\mforall{} (phi)sigma) \mvee{} psi) \mvdash{} \_ :Fiber(equiv-fun(((f)sigma)[1(\mBbbI{})]);a'1)\} 154. equiv-fun((((f)sigma)[1(\mBbbI{})])tau) \mmember{} \{K, (((phi)sigma)[1(\mBbbI{})])tau \mvdash{} \_:((((T)sigma)[1(\mBbbI{})])tau {}\mrightarrow{} (((A)sigma)[1(\mBbbI{})])tau)\} 155. K, (((phi)sigma)[1(\mBbbI{})])tau \mvdash{} Fiber(equiv-fun((((f)sigma)[1(\mBbbI{})])tau);(a'1)tau) \mwedge{} (fiber-point((st)tau;(sw)tau) \mmember{} \{K, (((phi)sigma)[1(\mBbbI{})])tau, (((\mforall{} (phi)sigma) \mvee{} psi))tau \mvdash{} \_ :Fiber(equiv-fun((((f)sigma)[1(\mBbbI{})])tau);(a'1)tau)\}) 156. \{K, (((phi)sigma)[1(\mBbbI{})])tau \mvdash{} \_:Fiber(equiv-fun((((f)sigma)[1(\mBbbI{})])tau);(a'1)tau) [(((\mforall{} (phi)sigma) \mvee{} psi))tau |{}\mrightarrow{} fiber-point((st)tau;(sw)tau)]\} \mmember{} \mBbbU{}\{[i' | j']\} 157. (equiv ((f)sigma)[1(\mBbbI{})] [((\mforall{} (phi)sigma) \mvee{} psi) \mvdash{}\mrightarrow{} (st, sw)] a'1)tau = equiv ((f)sigma o tau+)[1(\mBbbI{})] [((\mforall{} (phi)sigma o tau+) \mvee{} (psi)tau) \mvdash{}\mrightarrow{} (stt, sww)] aa'1 158. \{H, ((phi)sigma)[1(\mBbbI{})] \mvdash{} \_:Fiber(equiv-fun(((f)sigma)[1(\mBbbI{})]);a'1)[((\mforall{} (phi)sigma) \mvee{} psi) |{}\mrightarrow{} fiber-point(st;sw)]\} \mmember{} \mBbbU{}\{[i' | j']\} 159. z : \{H, ((phi)sigma)[1(\mBbbI{})] \mvdash{} \_:Fiber(equiv-fun(((f)sigma)[1(\mBbbI{})]);a'1)[((\mforall{} (phi)sigma) \mvee{} psi) |{}\mrightarrow{} fiber-point(st;sw)]\} 160. equiv ((f)sigma)[1(\mBbbI{})] [((\mforall{} (phi)sigma) \mvee{} psi) \mvdash{}\mrightarrow{} (st, sw)] a'1 = z 161. zz : \{K, (((phi)sigma)[1(\mBbbI{})])tau \mvdash{} \_:Fiber(equiv-fun((((f)sigma)[1(\mBbbI{})])tau);(a'1)tau) [(((\mforall{} (phi)sigma) \mvee{} psi))tau |{}\mrightarrow{} fiber-point((st)tau;(sw)tau)]\} 162. equiv ((f)sigma o tau+)[1(\mBbbI{})] [((\mforall{} (phi)sigma o tau+) \mvee{} (psi)tau) \mvdash{}\mrightarrow{} (stt, sww)] aa'1 = zz 163. (z)tau \mmember{} \{K, (((phi)sigma)[1(\mBbbI{})])tau \mvdash{} \_:(Fiber(equiv-fun(((f)sigma)[1(\mBbbI{})]);a'1))tau [(((\mforall{} (phi)sigma) \mvee{} psi))tau |{}\mrightarrow{} (fiber-point(st;sw))tau]\} \mvdash{} H, ((phi)sigma)[1(\mBbbI{})] \mvdash{} Fiber((equiv-fun((f)sigma))[1(\mBbbI{})];a'1) By Latex: MemCD Home Index