---

Step * of Lemma uabetatype_wf

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _:c𝕌}]. ∀[f:G:CubicalSet{i|j} ⟶ A:{G ⊢ _:c𝕌} ⟶ TransportType(A)].  G ⊢ uabetatype(G;A;B;f)
BY
{ ((Intros THEN (Assert G ⊢ Equiv(decode(A);decode(B)) BY Auto))
   THEN (Assert G.Equiv(decode(A);decode(B)) ⊢ (decode(A))p BY
               Auto)
   THEN (InstLemmaIJ  `path-type_wf` [⌜G.Equiv(decode(A);decode(B)).(decode(A))p⌝;⌜((decode(B))p)p⌝]⋅ THENA Auto)
   THEN (Assert (q)p ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((Equiv(decode(A);decode(B)))p)p} BY
               Auto)
   THEN (Assert (q)p ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:Equiv(((decode(A))p)p;((decode(B))p)p)} BY
               (InferEqualTypeGen THEN Auto THEN RWW "cubical-equiv-p<" 0 THEN Auto))
   THEN (Assert equiv-fun((q)p) ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _
                                   :(((decode(A))p)p ⟶ ((decode(B))p)p)} BY
               (MemCD THEN Auto))
   THEN (Assert app(equiv-fun((q)p); q) ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((decode(B))p)p} BY
               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}
⊢ G ⊢ uabetatype(G;A;B;f)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G  \mvdash{}  \_:c\mBbbU{}\}].  \mforall{}[f:G:CubicalSet\{i|j\}  {}\mrightarrow{}  A:\{G  \mvdash{}  \_:c\mBbbU{}\}  {}\mrightarrow{}  TransportType(A)].
    G  \mvdash{}  uabetatype(G;A;B;f)


By

---

Latex:
((Intros  THEN  (Assert  G  \mvdash{}  Equiv(decode(A);decode(B))  BY  Auto))
  THEN  (Assert  G.Equiv(decode(A);decode(B))  \mvdash{}  (decode(A))p  BY
                          Auto)
  THEN  (InstLemmaIJ    `path-type\_wf`  [\mkleeneopen{}G.Equiv(decode(A);decode(B)).(decode(A))p\mkleeneclose{};\mkleeneopen{}((decode(B))p)p\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  (Assert  (q)p  \mmember{}  \{G.Equiv(decode(A);decode(B)).(decode(A))p  \mvdash{}  \_
                                            :((Equiv(decode(A);decode(B)))p)p\}  BY
                          Auto)
  THEN  (Assert  (q)p  \mmember{}  \{G.Equiv(decode(A);decode(B)).(decode(A))p  \mvdash{}  \_
                                            :Equiv(((decode(A))p)p;((decode(B))p)p)\}  BY
                          (InferEqualTypeGen  THEN  Auto  THEN  RWW  "cubical-equiv-p<"  0  THEN  Auto))
  THEN  (Assert  equiv-fun((q)p)  \mmember{}  \{G.Equiv(decode(A);decode(B)).(decode(A))p  \mvdash{}  \_
                                                                  :(((decode(A))p)p  {}\mrightarrow{}  ((decode(B))p)p)\}  BY
                          (MemCD  THEN  Auto))
  THEN  (Assert  app(equiv-fun((q)p);  q)  \mmember{}  \{G.Equiv(decode(A);decode(B)).(decode(A))p  \mvdash{}  \_
                                                                                  :((decode(B))p)p\}  BY
                          Auto))

---

Home Index