Step
*
2
1
1
2
5
3
1
1
1
1
2
1
1
1
of Lemma
pres-constraint
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. A : {G.𝕀 ⊢ _}
4. T : {G.𝕀 ⊢ _}
5. f : {G.𝕀 ⊢ _:(T ⟶ A)}
6. t : {G.𝕀, (phi)p ⊢ _:T}
7. t0 : {G ⊢ _:(T)[0(𝕀)][phi |⟶ t[0]]}
8. cT : G.𝕀 +⊢ Compositon(T)
9. cA : G.𝕀 +⊢ Compositon(A)
10. pres f [phi ⊢→ t] t0 ∈ {G ⊢ _:(Path_(A)[1(𝕀)] pres-c1(G;phi;f;t;t0;cA) pres-c2(G;phi;f;t;t0;cT))}
11. p+ ∈ G.𝕀.𝕀 ij⟶ G.𝕀
12. app(f; t) ∈ {G.𝕀, (phi)p ⊢ _:A}
13. {G.𝕀.𝕀 ⊢ _:(A)p+} ⊆r {G.𝕀, ((phi)p ∨ (q=1)).𝕀 ⊢ _:(A)p+}
14. {G.𝕀 ⊢ _:((A)p+)[1(𝕀)][((phi)p ∨ (q=1)) |⟶ ((presw(G;phi;f;t;t0;cT))p+)[1(𝕀)]]} ∈ 𝕌{[i' | j']}
15. (presw(G;phi;f;t;t0;cT))p+ ∈ {G.𝕀, ((phi)p ∨ (q=1)).𝕀 ⊢ _:(A)p+}
16. (pres-a0(G;f;t0))p ∈ {G.𝕀 ⊢ _:((A)p+)[0(𝕀)][((phi)p ∨ (q=1)) |⟶ ((presw(G;phi;f;t;t0;cT))p+)[0(𝕀)]]}
17. comp (cA)p+ [((phi)p ∨ (q=1)) ⊢→ (presw(G;phi;f;t;t0;cT))p+] (pres-a0(G;f;t0))p
∈ {G.𝕀 ⊢ _:((A)p+)[1(𝕀)][((phi)p ∨ (q=1)) |⟶ ((presw(G;phi;f;t;t0;cT))p+)[1(𝕀)]]}
18. {G.𝕀 ⊢ _:((A)p+)[1(𝕀)][((phi)p ∨ (q=1)) |⟶ ((presw(G;phi;f;t;t0;cT))p+)[1(𝕀)]]} ⊆r {G.𝕀 ⊢ _:((A)[1(𝕀)])p}
19. ∀a:{G, phi.𝕀 ⊢ _:((A)[1(𝕀)])p}
(∀[b:{G, phi.𝕀 ⊢ _:((A)[1(𝕀)])p}]
G, phi ⊢ <>(a)
= G, phi ⊢ <>(b)
∈ {G, phi ⊢ _:(Path_(A)[1(𝕀)] pres-c1(G;phi;f;t;t0;cA) pres-c2(G;phi;f;t;t0;cT))}
supposing a = b ∈ {G, phi.𝕀 ⊢ _:((A)[1(𝕀)])p}) supposing
(G, phi ⊢ (a)[0(𝕀)]=pres-c1(G;phi;f;t;t0;cA):(A)[1(𝕀)] and
G, phi ⊢ (a)[1(𝕀)]=pres-c2(G;phi;f;t;t0;cT):(A)[1(𝕀)])
20. (comp (cA)p+ [((phi)p ∨ (q=1)) ⊢→ (presw(G;phi;f;t;t0;cT))p+] (pres-a0(G;f;t0))p)[0(𝕀)]
= comp ((cA)p+)[0(𝕀)]+ [(((phi)p ∨ (q=1)))[0(𝕀)] ⊢→ ((presw(G;phi;f;t;t0;cT))p+)[0(𝕀)]+] ((pres-a0(G;f;t0))p)[0(𝕀)]
∈ {G ⊢ _:(A)[1(𝕀)][(((phi)p ∨ (q=1)))[0(𝕀)] |⟶ (presw(G;phi;f;t;t0;cT))[1(𝕀)]]}
21. phi = (((phi)p ∨ (q=1)))[0(𝕀)] ∈ {G ⊢ _:𝔽}
22. v : {G.𝕀 ⊢ _:T}
23. t = v ∈ {G.𝕀, (phi)p ⊢ _:T}
⊢ app((f)[1(𝕀)]; (t)[1(𝕀)]) = app((f)[1(𝕀)]; (v)[1(𝕀)]) ∈ {G, phi ⊢ _:(A)[1(𝕀)]}
BY
{ GenConcl ⌜(f)[1(𝕀)] = f1 ∈ {G, phi ⊢ _:((T)[1(𝕀)] ⟶ (A)[1(𝕀)])}⌝⋅ }
1
.....wf.....
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. A : {G.𝕀 ⊢ _}
4. T : {G.𝕀 ⊢ _}
5. f : {G.𝕀 ⊢ _:(T ⟶ A)}
6. t : {G.𝕀, (phi)p ⊢ _:T}
7. t0 : {G ⊢ _:(T)[0(𝕀)][phi |⟶ t[0]]}
8. cT : G.𝕀 +⊢ Compositon(T)
9. cA : G.𝕀 +⊢ Compositon(A)
10. pres f [phi ⊢→ t] t0 ∈ {G ⊢ _:(Path_(A)[1(𝕀)] pres-c1(G;phi;f;t;t0;cA) pres-c2(G;phi;f;t;t0;cT))}
11. p+ ∈ G.𝕀.𝕀 ij⟶ G.𝕀
12. app(f; t) ∈ {G.𝕀, (phi)p ⊢ _:A}
13. {G.𝕀.𝕀 ⊢ _:(A)p+} ⊆r {G.𝕀, ((phi)p ∨ (q=1)).𝕀 ⊢ _:(A)p+}
14. {G.𝕀 ⊢ _:((A)p+)[1(𝕀)][((phi)p ∨ (q=1)) |⟶ ((presw(G;phi;f;t;t0;cT))p+)[1(𝕀)]]} ∈ 𝕌{[i' | j']}
15. (presw(G;phi;f;t;t0;cT))p+ ∈ {G.𝕀, ((phi)p ∨ (q=1)).𝕀 ⊢ _:(A)p+}
16. (pres-a0(G;f;t0))p ∈ {G.𝕀 ⊢ _:((A)p+)[0(𝕀)][((phi)p ∨ (q=1)) |⟶ ((presw(G;phi;f;t;t0;cT))p+)[0(𝕀)]]}
17. comp (cA)p+ [((phi)p ∨ (q=1)) ⊢→ (presw(G;phi;f;t;t0;cT))p+] (pres-a0(G;f;t0))p
∈ {G.𝕀 ⊢ _:((A)p+)[1(𝕀)][((phi)p ∨ (q=1)) |⟶ ((presw(G;phi;f;t;t0;cT))p+)[1(𝕀)]]}
18. {G.𝕀 ⊢ _:((A)p+)[1(𝕀)][((phi)p ∨ (q=1)) |⟶ ((presw(G;phi;f;t;t0;cT))p+)[1(𝕀)]]} ⊆r {G.𝕀 ⊢ _:((A)[1(𝕀)])p}
19. ∀a:{G, phi.𝕀 ⊢ _:((A)[1(𝕀)])p}
(∀[b:{G, phi.𝕀 ⊢ _:((A)[1(𝕀)])p}]
G, phi ⊢ <>(a)
= G, phi ⊢ <>(b)
∈ {G, phi ⊢ _:(Path_(A)[1(𝕀)] pres-c1(G;phi;f;t;t0;cA) pres-c2(G;phi;f;t;t0;cT))}
supposing a = b ∈ {G, phi.𝕀 ⊢ _:((A)[1(𝕀)])p}) supposing
(G, phi ⊢ (a)[0(𝕀)]=pres-c1(G;phi;f;t;t0;cA):(A)[1(𝕀)] and
G, phi ⊢ (a)[1(𝕀)]=pres-c2(G;phi;f;t;t0;cT):(A)[1(𝕀)])
20. (comp (cA)p+ [((phi)p ∨ (q=1)) ⊢→ (presw(G;phi;f;t;t0;cT))p+] (pres-a0(G;f;t0))p)[0(𝕀)]
= comp ((cA)p+)[0(𝕀)]+ [(((phi)p ∨ (q=1)))[0(𝕀)] ⊢→ ((presw(G;phi;f;t;t0;cT))p+)[0(𝕀)]+] ((pres-a0(G;f;t0))p)[0(𝕀)]
∈ {G ⊢ _:(A)[1(𝕀)][(((phi)p ∨ (q=1)))[0(𝕀)] |⟶ (presw(G;phi;f;t;t0;cT))[1(𝕀)]]}
21. phi = (((phi)p ∨ (q=1)))[0(𝕀)] ∈ {G ⊢ _:𝔽}
22. v : {G.𝕀 ⊢ _:T}
23. t = v ∈ {G.𝕀, (phi)p ⊢ _:T}
⊢ (f)[1(𝕀)] ∈ {G, phi ⊢ _:((T)[1(𝕀)] ⟶ (A)[1(𝕀)])}
2
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. A : {G.𝕀 ⊢ _}
4. T : {G.𝕀 ⊢ _}
5. f : {G.𝕀 ⊢ _:(T ⟶ A)}
6. t : {G.𝕀, (phi)p ⊢ _:T}
7. t0 : {G ⊢ _:(T)[0(𝕀)][phi |⟶ t[0]]}
8. cT : G.𝕀 +⊢ Compositon(T)
9. cA : G.𝕀 +⊢ Compositon(A)
10. pres f [phi ⊢→ t] t0 ∈ {G ⊢ _:(Path_(A)[1(𝕀)] pres-c1(G;phi;f;t;t0;cA) pres-c2(G;phi;f;t;t0;cT))}
11. p+ ∈ G.𝕀.𝕀 ij⟶ G.𝕀
12. app(f; t) ∈ {G.𝕀, (phi)p ⊢ _:A}
13. {G.𝕀.𝕀 ⊢ _:(A)p+} ⊆r {G.𝕀, ((phi)p ∨ (q=1)).𝕀 ⊢ _:(A)p+}
14. {G.𝕀 ⊢ _:((A)p+)[1(𝕀)][((phi)p ∨ (q=1)) |⟶ ((presw(G;phi;f;t;t0;cT))p+)[1(𝕀)]]} ∈ 𝕌{[i' | j']}
15. (presw(G;phi;f;t;t0;cT))p+ ∈ {G.𝕀, ((phi)p ∨ (q=1)).𝕀 ⊢ _:(A)p+}
16. (pres-a0(G;f;t0))p ∈ {G.𝕀 ⊢ _:((A)p+)[0(𝕀)][((phi)p ∨ (q=1)) |⟶ ((presw(G;phi;f;t;t0;cT))p+)[0(𝕀)]]}
17. comp (cA)p+ [((phi)p ∨ (q=1)) ⊢→ (presw(G;phi;f;t;t0;cT))p+] (pres-a0(G;f;t0))p
∈ {G.𝕀 ⊢ _:((A)p+)[1(𝕀)][((phi)p ∨ (q=1)) |⟶ ((presw(G;phi;f;t;t0;cT))p+)[1(𝕀)]]}
18. {G.𝕀 ⊢ _:((A)p+)[1(𝕀)][((phi)p ∨ (q=1)) |⟶ ((presw(G;phi;f;t;t0;cT))p+)[1(𝕀)]]} ⊆r {G.𝕀 ⊢ _:((A)[1(𝕀)])p}
19. ∀a:{G, phi.𝕀 ⊢ _:((A)[1(𝕀)])p}
(∀[b:{G, phi.𝕀 ⊢ _:((A)[1(𝕀)])p}]
G, phi ⊢ <>(a)
= G, phi ⊢ <>(b)
∈ {G, phi ⊢ _:(Path_(A)[1(𝕀)] pres-c1(G;phi;f;t;t0;cA) pres-c2(G;phi;f;t;t0;cT))}
supposing a = b ∈ {G, phi.𝕀 ⊢ _:((A)[1(𝕀)])p}) supposing
(G, phi ⊢ (a)[0(𝕀)]=pres-c1(G;phi;f;t;t0;cA):(A)[1(𝕀)] and
G, phi ⊢ (a)[1(𝕀)]=pres-c2(G;phi;f;t;t0;cT):(A)[1(𝕀)])
20. (comp (cA)p+ [((phi)p ∨ (q=1)) ⊢→ (presw(G;phi;f;t;t0;cT))p+] (pres-a0(G;f;t0))p)[0(𝕀)]
= comp ((cA)p+)[0(𝕀)]+ [(((phi)p ∨ (q=1)))[0(𝕀)] ⊢→ ((presw(G;phi;f;t;t0;cT))p+)[0(𝕀)]+] ((pres-a0(G;f;t0))p)[0(𝕀)]
∈ {G ⊢ _:(A)[1(𝕀)][(((phi)p ∨ (q=1)))[0(𝕀)] |⟶ (presw(G;phi;f;t;t0;cT))[1(𝕀)]]}
21. phi = (((phi)p ∨ (q=1)))[0(𝕀)] ∈ {G ⊢ _:𝔽}
22. v : {G.𝕀 ⊢ _:T}
23. t = v ∈ {G.𝕀, (phi)p ⊢ _:T}
24. f1 : {G, phi ⊢ _:((T)[1(𝕀)] ⟶ (A)[1(𝕀)])}
25. (f)[1(𝕀)] = f1 ∈ {G, phi ⊢ _:((T)[1(𝕀)] ⟶ (A)[1(𝕀)])}
⊢ app(f1; (t)[1(𝕀)]) = app(f1; (v)[1(𝕀)]) ∈ {G, phi ⊢ _:(A)[1(𝕀)]}
Latex:
Latex:
1. G : CubicalSet\{j\}
2. phi : \{G \mvdash{} \_:\mBbbF{}\}
3. A : \{G.\mBbbI{} \mvdash{} \_\}
4. T : \{G.\mBbbI{} \mvdash{} \_\}
5. f : \{G.\mBbbI{} \mvdash{} \_:(T {}\mrightarrow{} A)\}
6. t : \{G.\mBbbI{}, (phi)p \mvdash{} \_:T\}
7. t0 : \{G \mvdash{} \_:(T)[0(\mBbbI{})][phi |{}\mrightarrow{} t[0]]\}
8. cT : G.\mBbbI{} +\mvdash{} Compositon(T)
9. cA : G.\mBbbI{} +\mvdash{} Compositon(A)
10. pres f [phi \mvdash{}\mrightarrow{} t] t0 \mmember{} \{G \mvdash{} \_:(Path\_(A)[1(\mBbbI{})] pres-c1(G;phi;f;t;t0;cA)
pres-c2(G;phi;f;t;t0;cT))\}
11. p+ \mmember{} G.\mBbbI{}.\mBbbI{} ij{}\mrightarrow{} G.\mBbbI{}
12. app(f; t) \mmember{} \{G.\mBbbI{}, (phi)p \mvdash{} \_:A\}
13. \{G.\mBbbI{}.\mBbbI{} \mvdash{} \_:(A)p+\} \msubseteq{}r \{G.\mBbbI{}, ((phi)p \mvee{} (q=1)).\mBbbI{} \mvdash{} \_:(A)p+\}
14. \{G.\mBbbI{} \mvdash{} \_:((A)p+)[1(\mBbbI{})][((phi)p \mvee{} (q=1)) |{}\mrightarrow{} ((presw(G;phi;f;t;t0;cT))p+)[1(\mBbbI{})]]\} \mmember{} \mBbbU{}\{[i' | j']\}
15. (presw(G;phi;f;t;t0;cT))p+ \mmember{} \{G.\mBbbI{}, ((phi)p \mvee{} (q=1)).\mBbbI{} \mvdash{} \_:(A)p+\}
16. (pres-a0(G;f;t0))p \mmember{} \{G.\mBbbI{} \mvdash{} \_:((A)p+)[0(\mBbbI{})][((phi)p \mvee{} (q=1))
|{}\mrightarrow{} ((presw(G;phi;f;t;t0;cT))p+)[0(\mBbbI{})]]\}
17. comp (cA)p+ [((phi)p \mvee{} (q=1)) \mvdash{}\mrightarrow{} (presw(G;phi;f;t;t0;cT))p+] (pres-a0(G;f;t0))p
\mmember{} \{G.\mBbbI{} \mvdash{} \_:((A)p+)[1(\mBbbI{})][((phi)p \mvee{} (q=1)) |{}\mrightarrow{} ((presw(G;phi;f;t;t0;cT))p+)[1(\mBbbI{})]]\}
18. \{G.\mBbbI{} \mvdash{} \_:((A)p+)[1(\mBbbI{})][((phi)p \mvee{} (q=1)) |{}\mrightarrow{} ((presw(G;phi;f;t;t0;cT))p+)[1(\mBbbI{})]]\}
\msubseteq{}r \{G.\mBbbI{} \mvdash{} \_:((A)[1(\mBbbI{})])p\}
19. \mforall{}a:\{G, phi.\mBbbI{} \mvdash{} \_:((A)[1(\mBbbI{})])p\}
(\mforall{}[b:\{G, phi.\mBbbI{} \mvdash{} \_:((A)[1(\mBbbI{})])p\}]. G, phi \mvdash{} <>(a) = G, phi \mvdash{} <>(b) supposing a = b) supposing
(G, phi \mvdash{} (a)[0(\mBbbI{})]=pres-c1(G;phi;f;t;t0;cA):(A)[1(\mBbbI{})] and
G, phi \mvdash{} (a)[1(\mBbbI{})]=pres-c2(G;phi;f;t;t0;cT):(A)[1(\mBbbI{})])
20. (comp (cA)p+ [((phi)p \mvee{} (q=1)) \mvdash{}\mrightarrow{} (presw(G;phi;f;t;t0;cT))p+] (pres-a0(G;f;t0))p)[0(\mBbbI{})]
= comp ((cA)p+)[0(\mBbbI{})]+ [(((phi)p \mvee{} (q=1)))[0(\mBbbI{})] \mvdash{}\mrightarrow{} ((presw(G;phi;f;t;t0;cT))p+)[0(\mBbbI{})]+]
((pres-a0(G;f;t0))p)[0(\mBbbI{})]
21. phi = (((phi)p \mvee{} (q=1)))[0(\mBbbI{})]
22. v : \{G.\mBbbI{} \mvdash{} \_:T\}
23. t = v
\mvdash{} app((f)[1(\mBbbI{})]; (t)[1(\mBbbI{})]) = app((f)[1(\mBbbI{})]; (v)[1(\mBbbI{})])
By
Latex:
GenConcl \mkleeneopen{}(f)[1(\mBbbI{})] = f1\mkleeneclose{}\mcdot{}
Home
Index