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

.....assertion..... 
1. CubicalSet{j}
2. {G ⊢ _}
3. cA +⊢ Compositon(A)
4. phi {G ⊢ _:𝔽}
5. {G, phi ⊢ _}
6. cT G, phi +⊢ Compositon(T)
7. {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. CubicalSet{j}
10. CubicalSet{j}
11. tau j⟶ H
12. sigma H.𝕀 j⟶ G
13. psi {H ⊢ _:𝔽}
14. {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 ⊢ _} ⊆{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) ⊆H, (∀ (phi)sigma).𝕀 +⊢ Compositon((T)sigma)
28. H.𝕀(phi)sigma +⊢ Compositon((A)sigma) ⊆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(𝕀)] ⊢ _} ⊆{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(𝕀)] ⊢ _} ⊆{H, (∀ (phi)sigma) ⊢ _}
42. H, (∀ (phi)sigma) ⊢ ((T)sigma)[1(𝕀)]
43. {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(𝕀)] ⊢ _} ⊆{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 tau+)
69. sub_cubical_set{j:l}(K, ((∀ (phi)sigma))tau.𝕀K.𝕀((phi)sigma)tau+)
70. {K.𝕀((phi)sigma)tau+ ⊢ _} ⊆{K, ((∀ (phi)sigma))tau.𝕀 ⊢ _}
71. K, ((∀ (phi)sigma))tau.𝕀 ⊢ ((T)sigma)tau+
72. (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(𝕀)]]}
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 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']}
⊢ (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+))}
BY
((Assert ⌜pres ((equiv-fun(f))sigma)tau+ [(psi)tau ⊢→ (b)tau+] (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+))}⌝⋅
   THENM Eq
   )
   THEN (Subst' (equiv-fun(f))sigma tau+ ((equiv-fun(f))sigma)tau+ 0
         THENA ((RWW  "csm-equiv-fun" THENA Auto) THEN CsmUnfolding THEN Auto)
         )
   THEN (RWO  "cubical-fun-subset" (-5) THEN Try (Trivial))
   THEN (Subst' (cT)sigma tau+ ((cT)sigma)tau+ THENA (RepUR ``csm-comp-structure`` THEN CsmUnfolding THEN Auto))
   THEN (Subst' (cA)sigma tau+ ((cA)sigma)tau+ THENA (RepUR ``csm-comp-structure`` THEN CsmUnfolding THEN Auto))
   THEN (Subst' (b)tau+ (b)tau+ THENA (CsmUnfolding THEN Auto))
   THEN BLemma `pres-invariant`
   THEN Try (QuickAuto)) }

1
.....wf..... 
1. CubicalSet{j}
2. {G ⊢ _}
3. cA +⊢ Compositon(A)
4. phi {G ⊢ _:𝔽}
5. {G, phi ⊢ _}
6. cT G, phi +⊢ Compositon(T)
7. {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. CubicalSet{j}
10. CubicalSet{j}
11. tau j⟶ H
12. sigma H.𝕀 j⟶ G
13. psi {H ⊢ _:𝔽}
14. {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 ⊢ _} ⊆{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) ⊆H, (∀ (phi)sigma).𝕀 +⊢ Compositon((T)sigma)
28. H.𝕀(phi)sigma +⊢ Compositon((A)sigma) ⊆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(𝕀)] ⊢ _} ⊆{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(𝕀)] ⊢ _} ⊆{H, (∀ (phi)sigma) ⊢ _}
42. H, (∀ (phi)sigma) ⊢ ((T)sigma)[1(𝕀)]
43. {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(𝕀)] ⊢ _} ⊆{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 tau+)
69. sub_cubical_set{j:l}(K, ((∀ (phi)sigma))tau.𝕀K.𝕀((phi)sigma)tau+)
70. {K.𝕀((phi)sigma)tau+ ⊢ _} ⊆{K, ((∀ (phi)sigma))tau.𝕀 ⊢ _}
71. K, ((∀ (phi)sigma))tau.𝕀 ⊢ ((T)sigma)tau+
72. (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(𝕀)]]}
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 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']}
⊢ (b)tau+ ∈ {K, ((∀ (phi)sigma))tau.𝕀((psi)tau)p ⊢ _:((T)sigma)tau+}

2
.....wf..... 
1. CubicalSet{j}
2. {G ⊢ _}
3. cA +⊢ Compositon(A)
4. phi {G ⊢ _:𝔽}
5. {G, phi ⊢ _}
6. cT G, phi +⊢ Compositon(T)
7. {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. CubicalSet{j}
10. CubicalSet{j}
11. tau j⟶ H
12. sigma H.𝕀 j⟶ G
13. psi {H ⊢ _:𝔽}
14. {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 ⊢ _} ⊆{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) ⊆H, (∀ (phi)sigma).𝕀 +⊢ Compositon((T)sigma)
28. H.𝕀(phi)sigma +⊢ Compositon((A)sigma) ⊆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(𝕀)] ⊢ _} ⊆{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(𝕀)] ⊢ _} ⊆{H, (∀ (phi)sigma) ⊢ _}
42. H, (∀ (phi)sigma) ⊢ ((T)sigma)[1(𝕀)]
43. {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(𝕀)] ⊢ _} ⊆{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 tau+)
69. sub_cubical_set{j:l}(K, ((∀ (phi)sigma))tau.𝕀K.𝕀((phi)sigma)tau+)
70. {K.𝕀((phi)sigma)tau+ ⊢ _} ⊆{K, ((∀ (phi)sigma))tau.𝕀 ⊢ _}
71. K, ((∀ (phi)sigma))tau.𝕀 ⊢ ((T)sigma)tau+
72. (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(𝕀)]]}
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 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']}
⊢ (b0)tau ∈ {K, ((∀ (phi)sigma))tau ⊢ _:(((T)sigma)tau+)[0(𝕀)][(psi)tau |⟶ (b)tau+[0]]}

3
.....wf..... 
1. CubicalSet{j}
2. {G ⊢ _}
3. cA +⊢ Compositon(A)
4. phi {G ⊢ _:𝔽}
5. {G, phi ⊢ _}
6. cT G, phi +⊢ Compositon(T)
7. {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. CubicalSet{j}
10. CubicalSet{j}
11. tau j⟶ H
12. sigma H.𝕀 j⟶ G
13. psi {H ⊢ _:𝔽}
14. {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 ⊢ _} ⊆{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) ⊆H, (∀ (phi)sigma).𝕀 +⊢ Compositon((T)sigma)
28. H.𝕀(phi)sigma +⊢ Compositon((A)sigma) ⊆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(𝕀)] ⊢ _} ⊆{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(𝕀)] ⊢ _} ⊆{H, (∀ (phi)sigma) ⊢ _}
42. H, (∀ (phi)sigma) ⊢ ((T)sigma)[1(𝕀)]
43. {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(𝕀)] ⊢ _} ⊆{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 tau+)
69. sub_cubical_set{j:l}(K, ((∀ (phi)sigma))tau.𝕀K.𝕀((phi)sigma)tau+)
70. {K.𝕀((phi)sigma)tau+ ⊢ _} ⊆{K, ((∀ (phi)sigma))tau.𝕀 ⊢ _}
71. K, ((∀ (phi)sigma))tau.𝕀 ⊢ ((T)sigma)tau+
72. (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(𝕀)]]}
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 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']}
⊢ ((cT)sigma)tau+ ∈ K, ((∀ (phi)sigma))tau.𝕀 +⊢ Compositon(((T)sigma)tau+)

4
.....wf..... 
1. CubicalSet{j}
2. {G ⊢ _}
3. cA +⊢ Compositon(A)
4. phi {G ⊢ _:𝔽}
5. {G, phi ⊢ _}
6. cT G, phi +⊢ Compositon(T)
7. {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. CubicalSet{j}
10. CubicalSet{j}
11. tau j⟶ H
12. sigma H.𝕀 j⟶ G
13. psi {H ⊢ _:𝔽}
14. {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 ⊢ _} ⊆{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) ⊆H, (∀ (phi)sigma).𝕀 +⊢ Compositon((T)sigma)
28. H.𝕀(phi)sigma +⊢ Compositon((A)sigma) ⊆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(𝕀)] ⊢ _} ⊆{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(𝕀)] ⊢ _} ⊆{H, (∀ (phi)sigma) ⊢ _}
42. H, (∀ (phi)sigma) ⊢ ((T)sigma)[1(𝕀)]
43. {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(𝕀)] ⊢ _} ⊆{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 tau+)
69. sub_cubical_set{j:l}(K, ((∀ (phi)sigma))tau.𝕀K.𝕀((phi)sigma)tau+)
70. {K.𝕀((phi)sigma)tau+ ⊢ _} ⊆{K, ((∀ (phi)sigma))tau.𝕀 ⊢ _}
71. K, ((∀ (phi)sigma))tau.𝕀 ⊢ ((T)sigma)tau+
72. (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(𝕀)]]}
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 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']}
⊢ ((cA)sigma)tau+ ∈ K, ((∀ (phi)sigma))tau.𝕀 +⊢ Compositon(((A)sigma)tau+)


Latex:


Latex:
.....assertion..... 
1.  G  :  CubicalSet\{j\}
2.  A  :  \{G  \mvdash{}  \_\}
3.  cA  :  G  +\mvdash{}  Compositon(A)
4.  phi  :  \{G  \mvdash{}  \_:\mBbbF{}\}
5.  T  :  \{G,  phi  \mvdash{}  \_\}
6.  cT  :  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']\}
\mvdash{}  (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


By


Latex:
((Assert  \mkleeneopen{}pres  ((equiv-fun(f))sigma)tau+  [(psi)tau  \mvdash{}\mrightarrow{}  (b)tau+]  (b0)tau
                    =  pres  (equiv-fun(f))sigma  o  tau+  [(psi)tau  \mvdash{}\mrightarrow{}  (b)tau+]  (b0)tau\mkleeneclose{}\mcdot{}
  THENM  Eq
  )
  THEN  (Subst'  (equiv-fun(f))sigma  o  tau+  \msim{}  ((equiv-fun(f))sigma)tau+  0
              THENA  ((RWW    "csm-equiv-fun"  0  THENA  Auto)  THEN  CsmUnfolding  THEN  Auto)
              )
  THEN  (RWO    "cubical-fun-subset"  (-5)  THEN  Try  (Trivial))
  THEN  (Subst'  (cT)sigma  o  tau+  \msim{}  ((cT)sigma)tau+  0
              THENA  (RepUR  ``csm-comp-structure``  0  THEN  CsmUnfolding  THEN  Auto)
              )
  THEN  (Subst'  (cA)sigma  o  tau+  \msim{}  ((cA)sigma)tau+  0
              THENA  (RepUR  ``csm-comp-structure``  0  THEN  CsmUnfolding  THEN  Auto)
              )
  THEN  (Subst'  (b)tau+  \msim{}  (b)tau+  0  THENA  (CsmUnfolding  THEN  Auto))
  THEN  BLemma  `pres-invariant`
  THEN  Try  (QuickAuto))




Home Index