Step
*
1
1
of Lemma
csm-trans-equiv-path
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. f : {G ⊢ _:Equiv(decode(A);decode(B))}
5. H : CubicalSet{j}
6. s : H j⟶ G
7. (A)s ∈ {H ⊢ _:c𝕌}
8. (B)s ∈ {H ⊢ _:c𝕌}
9. G ⊢ Equiv(decode(A);decode(B))
10. G ⊢ decode(A)
11. G ⊢ decode(B)
12. (f)p ∈ {G.decode(A) ⊢ _:Equiv((decode(A))p;(decode(B))p)}
13. q ∈ {G.decode(A) ⊢ _:(decode(A))p}
14. G.decode(A) ⊢ (decode(B))p
15. (CompFun(B))p ∈ composition-structure{[[i | j] | [j | i]]:l, [i | j]:l}(G.decode(A); (decode(B))p)
16. (cubical-lam(G;transprt-const(G.decode(A);(CompFun(B))p;transprt-const(G.decode(A);(CompFun(B))p;app(equiv-fun(...);
q)))))s
= cubical-lam(H;(transprt-const(G.decode(A);(CompFun(B))p;transprt-const(G.decode(A);(CompFun(B))p;app(equiv-fun((f)p);
q))))s+)
∈ {H ⊢ _:((decode(A) ⟶ decode(B)))s}
⊢ (cubical-lam(G;transprt-const(G.decode(A);(CompFun(B))p;transprt-const(G.decode(A);(CompFun(B))p;app(equiv-fun((f)p);
q)))))s
= cubical-lam(H;transprt-const(H.decode((A)s);(CompFun((B)s))p;transprt-const(H.decode((A)s);(CompFun((B)s))p;app(...;
q))))
∈ {H ⊢ _:(decode((A)s) ⟶ decode((B)s))}
BY
{ SubsumeC ⌜{H ⊢ _:((decode(A) ⟶ decode(B)))s}⌝⋅ }
1
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. f : {G ⊢ _:Equiv(decode(A);decode(B))}
5. H : CubicalSet{j}
6. s : H j⟶ G
7. (A)s ∈ {H ⊢ _:c𝕌}
8. (B)s ∈ {H ⊢ _:c𝕌}
9. G ⊢ Equiv(decode(A);decode(B))
10. G ⊢ decode(A)
11. G ⊢ decode(B)
12. (f)p ∈ {G.decode(A) ⊢ _:Equiv((decode(A))p;(decode(B))p)}
13. q ∈ {G.decode(A) ⊢ _:(decode(A))p}
14. G.decode(A) ⊢ (decode(B))p
15. (CompFun(B))p ∈ composition-structure{[[i | j] | [j | i]]:l, [i | j]:l}(G.decode(A); (decode(B))p)
16. (cubical-lam(G;transprt-const(G.decode(A);(CompFun(B))p;transprt-const(G.decode(A);(CompFun(B))p;app(equiv-fun(...);
q)))))s
= cubical-lam(H;(transprt-const(G.decode(A);(CompFun(B))p;transprt-const(G.decode(A);(CompFun(B))p;app(equiv-fun((f)p);
q))))s+)
∈ {H ⊢ _:((decode(A) ⟶ decode(B)))s}
⊢ (cubical-lam(G;transprt-const(G.decode(A);(CompFun(B))p;transprt-const(G.decode(A);(CompFun(B))p;app(equiv-fun((f)p);
q)))))s
= cubical-lam(H;transprt-const(H.decode((A)s);(CompFun((B)s))p;transprt-const(H.decode((A)s);(CompFun((B)s))p;app(...;
q))))
∈ {H ⊢ _:((decode(A) ⟶ decode(B)))s}
2
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. f : {G ⊢ _:Equiv(decode(A);decode(B))}
5. H : CubicalSet{j}
6. s : H j⟶ G
7. (A)s ∈ {H ⊢ _:c𝕌}
8. (B)s ∈ {H ⊢ _:c𝕌}
9. G ⊢ Equiv(decode(A);decode(B))
10. G ⊢ decode(A)
11. G ⊢ decode(B)
12. (f)p ∈ {G.decode(A) ⊢ _:Equiv((decode(A))p;(decode(B))p)}
13. q ∈ {G.decode(A) ⊢ _:(decode(A))p}
14. G.decode(A) ⊢ (decode(B))p
15. (CompFun(B))p ∈ composition-structure{[[i | j] | [j | i]]:l, [i | j]:l}(G.decode(A); (decode(B))p)
16. (cubical-lam(G;transprt-const(G.decode(A);(CompFun(B))p;transprt-const(G.decode(A);(CompFun(B))p;app(equiv-fun(...);
q)))))s
= cubical-lam(H;(transprt-const(G.decode(A);(CompFun(B))p;transprt-const(G.decode(A);(CompFun(B))p;app(equiv-fun((f)p);
q))))s+)
∈ {H ⊢ _:((decode(A) ⟶ decode(B)))s}
17. (cubical-lam(G;transprt-const(G.decode(A);(CompFun(B))p;transprt-const(G.decode(A);(CompFun(B))p;app(equiv-fun(...);
q)))))s
= cubical-lam(H;transprt-const(H.decode((A)s);(CompFun((B)s))p;transprt-const(H.decode((A)s);(CompFun((B)s))p;app(...;
q))))
∈ {H ⊢ _:((decode(A) ⟶ decode(B)))s}
⊢ {H ⊢ _:((decode(A) ⟶ decode(B)))s} ⊆r {H ⊢ _:(decode((A)s) ⟶ decode((B)s))}
Latex:
Latex:
1. G : CubicalSet\{j\}
2. A : \{G \mvdash{} \_:c\mBbbU{}\}
3. B : \{G \mvdash{} \_:c\mBbbU{}\}
4. f : \{G \mvdash{} \_:Equiv(decode(A);decode(B))\}
5. H : CubicalSet\{j\}
6. s : H j{}\mrightarrow{} G
7. (A)s \mmember{} \{H \mvdash{} \_:c\mBbbU{}\}
8. (B)s \mmember{} \{H \mvdash{} \_:c\mBbbU{}\}
9. G \mvdash{} Equiv(decode(A);decode(B))
10. G \mvdash{} decode(A)
11. G \mvdash{} decode(B)
12. (f)p \mmember{} \{G.decode(A) \mvdash{} \_:Equiv((decode(A))p;(decode(B))p)\}
13. q \mmember{} \{G.decode(A) \mvdash{} \_:(decode(A))p\}
14. G.decode(A) \mvdash{} (decode(B))p
15. (CompFun(B))p \mmember{} composition-structure\{[[i | j] | [j | i]]:l, [i | j]:l\}(G.decode(A);
(decode(B))p)
16. (cubical-lam(G;transprt-const(G.decode(A);(CompFun(B))p;transprt-const(G.decode(A);...;...))))s
= cubical-lam(H;(transprt-const(G.decode(A);(CompFun(B))p;transprt-const(G.decode(A);...;...)))s+)
\mvdash{} (cubical-lam(G;transprt-const(G.decode(A);(CompFun(B))p;transprt-const(G.decode(A);(...)p;...))))s
= cubical-lam(H;transprt-const(H.decode((A)s);(CompFun((B)s))p;transprt-const(H....;(...)p;app(...;
q))))
By
Latex:
SubsumeC \mkleeneopen{}\{H \mvdash{} \_:((decode(A) {}\mrightarrow{} decode(B)))s\}\mkleeneclose{}\mcdot{}
Home
Index