Step
*
1
1
1
1
1
of Lemma
presw-pres-c1
.....assertion.....
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. p+ ∈ G.𝕀.𝕀 ij⟶ G.𝕀
11. app(f; t) ∈ {G.𝕀, (phi)p ⊢ _:A}
12. {G.𝕀.𝕀 ⊢ _:(A)p+} ⊆r {G.𝕀, ((phi)p ∨ (q=1)).𝕀 ⊢ _:(A)p+}
13. {G.𝕀 ⊢ _:((A)p+)[1(𝕀)][((phi)p ∨ (q=1)) |⟶ ((presw(G;phi;f;t;t0;cT))p+)[1(𝕀)]]} ∈ 𝕌{[i' | j']}
14. (presw(G;phi;f;t;t0;cT))p+ ∈ {G.𝕀, ((phi)p ∨ (q=1)).𝕀 ⊢ _:(A)p+}
15. (pres-a0(G;f;t0))p ∈ {G.𝕀 ⊢ _:((A)p+)[0(𝕀)][((phi)p ∨ (q=1)) |⟶ ((presw(G;phi;f;t;t0;cT))p+)[0(𝕀)]]}
16. 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(𝕀)]]}
17. (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(𝕀)]]}
⊢ phi = (((phi)p ∨ (q=1)))[0(𝕀)] ∈ {G ⊢ _:𝔽}
BY
{ (RWO "csm-face-or" 0 THENA Auto) }
1
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. p+ ∈ G.𝕀.𝕀 ij⟶ G.𝕀
11. app(f; t) ∈ {G.𝕀, (phi)p ⊢ _:A}
12. {G.𝕀.𝕀 ⊢ _:(A)p+} ⊆r {G.𝕀, ((phi)p ∨ (q=1)).𝕀 ⊢ _:(A)p+}
13. {G.𝕀 ⊢ _:((A)p+)[1(𝕀)][((phi)p ∨ (q=1)) |⟶ ((presw(G;phi;f;t;t0;cT))p+)[1(𝕀)]]} ∈ 𝕌{[i' | j']}
14. (presw(G;phi;f;t;t0;cT))p+ ∈ {G.𝕀, ((phi)p ∨ (q=1)).𝕀 ⊢ _:(A)p+}
15. (pres-a0(G;f;t0))p ∈ {G.𝕀 ⊢ _:((A)p+)[0(𝕀)][((phi)p ∨ (q=1)) |⟶ ((presw(G;phi;f;t;t0;cT))p+)[0(𝕀)]]}
16. 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(𝕀)]]}
17. (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(𝕀)]]}
⊢ phi = (((phi)p)[0(𝕀)] ∨ ((q=1))[0(𝕀)]) ∈ {G ⊢ _:𝔽}
Latex:
Latex:
.....assertion.....
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. p+ \mmember{} G.\mBbbI{}.\mBbbI{} ij{}\mrightarrow{} G.\mBbbI{}
11. app(f; t) \mmember{} \{G.\mBbbI{}, (phi)p \mvdash{} \_:A\}
12. \{G.\mBbbI{}.\mBbbI{} \mvdash{} \_:(A)p+\} \msubseteq{}r \{G.\mBbbI{}, ((phi)p \mvee{} (q=1)).\mBbbI{} \mvdash{} \_:(A)p+\}
13. \{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']\}
14. (presw(G;phi;f;t;t0;cT))p+ \mmember{} \{G.\mBbbI{}, ((phi)p \mvee{} (q=1)).\mBbbI{} \mvdash{} \_:(A)p+\}
15. (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{})]]\}
16. 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{})]]\}
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)[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{})]
\mvdash{} phi = (((phi)p \mvee{} (q=1)))[0(\mBbbI{})]
By
Latex:
(RWO "csm-face-or" 0 THENA Auto)
Home
Index