Step
*
1
of Lemma
uabetatype_wf
1. [G] : CubicalSet{j}
2. [A] : {G ⊢ _:c𝕌}
3. [B] : {G ⊢ _:c𝕌}
4. [f] : G:CubicalSet{i|j} ⟶ A:{G ⊢ _:c𝕌} ⟶ TransportType(A)
5. G ⊢ Equiv(decode(A);decode(B))
6. G.Equiv(decode(A);decode(B)) ⊢ (decode(A))p
7. ∀[a,b:{G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((decode(B))p)p}].
G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ (Path_((decode(B))p)p a b)
8. (q)p ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((Equiv(decode(A);decode(B)))p)p}
9. (q)p ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:Equiv(((decode(A))p)p;((decode(B))p)p)}
10. equiv-fun((q)p) ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:(((decode(A))p)p ⟶ ((decode(B))p)p)}
11. app(equiv-fun((q)p); q) ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((decode(B))p)p}
⊢ G ⊢ uabetatype(G;A;B;f)
BY
{ ((InstLemmaIJ `univ-a_wf`
[⌜G.Equiv(decode(A);decode(B)).(decode(A))p⌝;⌜((A)p)p⌝;⌜((B)p)p⌝]⋅
THENA (Repeat (BLemma `cubical-universe-p`) THEN Auto)
)
THEN (Assert app(UA; (q)p) ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:(Path_c𝕌 ((A)p)p ((B)p)p)} BY
(InstLemma `cubical-app_wf_fun` [⌜parm{i|j}⌝;⌜parm{i'}⌝]⋅
THEN BHyp -1
THEN Try (Trivial)
THEN ((NthHypSq (-2)
THEN RepeatFor 4 ((EqCD THEN Try (Trivial)))
THEN RWO "csm-universe-decode" 0
THEN Auto)
ORELSE (MemCD THEN Repeat (BLemma `cubical-universe-p`) THEN Auto)
)))
) }
1
1. [G] : CubicalSet{j}
2. [A] : {G ⊢ _:c𝕌}
3. [B] : {G ⊢ _:c𝕌}
4. [f] : G:CubicalSet{i|j} ⟶ A:{G ⊢ _:c𝕌} ⟶ TransportType(A)
5. G ⊢ Equiv(decode(A);decode(B))
6. G.Equiv(decode(A);decode(B)) ⊢ (decode(A))p
7. ∀[a,b:{G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((decode(B))p)p}].
G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ (Path_((decode(B))p)p a b)
8. (q)p ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((Equiv(decode(A);decode(B)))p)p}
9. (q)p ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:Equiv(((decode(A))p)p;((decode(B))p)p)}
10. equiv-fun((q)p) ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:(((decode(A))p)p ⟶ ((decode(B))p)p)}
11. app(equiv-fun((q)p); q) ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((decode(B))p)p}
12. UA ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _
:(Equiv(decode(((A)p)p);decode(((B)p)p)) ⟶ (Path_c𝕌 ((A)p)p ((B)p)p))}
13. app(UA; (q)p) ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:(Path_c𝕌 ((A)p)p ((B)p)p)}
⊢ G ⊢ uabetatype(G;A;B;f)
Latex:
Latex:
1. [G] : CubicalSet\{j\}
2. [A] : \{G \mvdash{} \_:c\mBbbU{}\}
3. [B] : \{G \mvdash{} \_:c\mBbbU{}\}
4. [f] : G:CubicalSet\{i|j\} {}\mrightarrow{} A:\{G \mvdash{} \_:c\mBbbU{}\} {}\mrightarrow{} TransportType(A)
5. G \mvdash{} Equiv(decode(A);decode(B))
6. G.Equiv(decode(A);decode(B)) \mvdash{} (decode(A))p
7. \mforall{}[a,b:\{G.Equiv(decode(A);decode(B)).(decode(A))p \mvdash{} \_:((decode(B))p)p\}].
G.Equiv(decode(A);decode(B)).(decode(A))p \mvdash{} (Path\_((decode(B))p)p a b)
8. (q)p \mmember{} \{G.Equiv(decode(A);decode(B)).(decode(A))p \mvdash{} \_:((Equiv(decode(A);decode(B)))p)p\}
9. (q)p \mmember{} \{G.Equiv(decode(A);decode(B)).(decode(A))p \mvdash{} \_:Equiv(((decode(A))p)p;((decode(B))p)p)\}
10. equiv-fun((q)p) \mmember{} \{G.Equiv(decode(A);decode(B)).(decode(A))p \mvdash{} \_
:(((decode(A))p)p {}\mrightarrow{} ((decode(B))p)p)\}
11. app(equiv-fun((q)p); q) \mmember{} \{G.Equiv(decode(A);decode(B)).(decode(A))p \mvdash{} \_:((decode(B))p)p\}
\mvdash{} G \mvdash{} uabetatype(G;A;B;f)
By
Latex:
((InstLemmaIJ `univ-a\_wf`
[\mkleeneopen{}G.Equiv(decode(A);decode(B)).(decode(A))p\mkleeneclose{};\mkleeneopen{}((A)p)p\mkleeneclose{};\mkleeneopen{}((B)p)p\mkleeneclose{}]\mcdot{}
THENA (Repeat (BLemma `cubical-universe-p`) THEN Auto)
)
THEN (Assert app(UA; (q)p) \mmember{} \{G.Equiv(decode(A);decode(B)).(decode(A))p \mvdash{} \_
:(Path\_c\mBbbU{} ((A)p)p ((B)p)p)\} BY
(InstLemma `cubical-app\_wf\_fun` [\mkleeneopen{}parm\{i|j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{}]\mcdot{}
THEN BHyp -1
THEN Try (Trivial)
THEN ((NthHypSq (-2)
THEN RepeatFor 4 ((EqCD THEN Try (Trivial)))
THEN RWO "csm-universe-decode" 0
THEN Auto)
ORELSE (MemCD THEN Repeat (BLemma `cubical-universe-p`) THEN Auto)
)))
)
Home
Index