Step
*
1
1
of Lemma
csm-presw
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. H : CubicalSet{j}
10. s : H jā¶ G
11. g : {H.š ā¢ _:((T)s+ ā¶ (A)s+)}
12. (f)s+ = g ā {H.š ā¢ _:((T)s+ ā¶ (A)s+)}
ā¢ (pres-v(G;phi;t;t0;cT))s+ = pres-v(H;(phi)s;(t)s+;(t0)s;(cT)s+) ā {H.š ā¢ _:(T)s+}
BY
{ (Enough to prove (pres-v(G;phi;t;t0;cT))s+
= pres-v(H;(phi)s;(t)s+;(t0)s;(cT)s+)
ā {H.š ā¢ _:(T)s+[((phi)s)p |ā¶ (t)s+]}
Because (EqTypeHD (-1) THEN 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. H : CubicalSet{j}
10. s : H jā¶ G
11. g : {H.š ā¢ _:((T)s+ ā¶ (A)s+)}
12. (f)s+ = g ā {H.š ā¢ _:((T)s+ ā¶ (A)s+)}
ā¢ (pres-v(G;phi;t;t0;cT))s+ = pres-v(H;(phi)s;(t)s+;(t0)s;(cT)s+) ā {H.š ā¢ _:(T)s+[((phi)s)p |ā¶ (t)s+]}
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. H : CubicalSet\{j\}
10. s : H j{}\mrightarrow{} G
11. g : \{H.\mBbbI{} \mvdash{} \_:((T)s+ {}\mrightarrow{} (A)s+)\}
12. (f)s+ = g
\mvdash{} (pres-v(G;phi;t;t0;cT))s+ = pres-v(H;(phi)s;(t)s+;(t0)s;(cT)s+)
By
Latex:
(Enough to prove (pres-v(G;phi;t;t0;cT))s+ = pres-v(H;(phi)s;(t)s+;(t0)s;(cT)s+)
Because (EqTypeHD (-1) THEN Auto))
Home
Index