Step
*
1
of Lemma
pres-constraint
.....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. 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+}
⊢ (pres-a0(G;f;t0))p ∈ {G.𝕀 ⊢ _:((A)p+)[0(𝕀)][((phi)p ∨ (q=1)) |⟶ ((presw(G;phi;f;t;t0;cT))p+)[0(𝕀)]]}
BY
{ MemTypeCD }
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. 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+}
⊢ (pres-a0(G;f;t0))p ∈ {G.𝕀 ⊢ _:((A)p+)[0(𝕀)]}
2
.....set predicate.....
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+}
⊢ ((presw(G;phi;f;t;t0;cT))p+)[0(𝕀)] = (pres-a0(G;f;t0))p ∈ {G.𝕀, ((phi)p ∨ (q=1)) ⊢ _:((A)p+)[0(𝕀)]}
3
.....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. a : {G.𝕀 ⊢ _:((A)p+)[0(𝕀)]}
⊢ istype(((presw(G;phi;f;t;t0;cT))p+)[0(𝕀)] = a ∈ {G.𝕀, ((phi)p ∨ (q=1)) ⊢ _:((A)p+)[0(𝕀)]})
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. 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+\}
\mvdash{} (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{})]]\}
By
Latex:
MemTypeCD
Home
Index