---

Step * of Lemma uabeta_wf

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _:c𝕌}].  (uabeta(G;A;B) ∈ {G ⊢ _:uabeta-type(G;A;B)})
BY
{ ((Intros⋅
    THEN (Assert G ⊢ decode(A) BY
                Auto)
    THEN (Assert (A)p ∈ {G.decode(A) ⊢ _:c𝕌} BY
                (BLemma `csm-ap-term-universe` THEN Auto))
    THEN (Assert G ⊢ decode(B) BY
                Auto)
    THEN (Assert (B)p ∈ {G.decode(A) ⊢ _:c𝕌} BY
                (BLemma `csm-ap-term-universe` THEN Auto))
    THEN (Assert G ⊢ Equiv(decode(A);decode(B)) BY
                Auto)
    THEN (Assert G.decode(A) ⊢ Equiv((decode(A))p;(decode(B))p) BY
                (RWO "csm-universe-decode" 0 THEN Auto)))
   THEN Unfold `uabeta-type` 0
   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 EqCDA THEN InstLemmaIJ `cubical-equiv-p` [] THEN RWW "-1<" 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
                Auto)
         THEN (Assert app(equiv-fun((q)p); q) ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((decode(B))p)p} BY
                     Auto)
         THEN (InstLemmaIJ `csm-ap-term-universe` [⌜G⌝;⌜G.Equiv(decode(A);decode(B))⌝;⌜p⌝]⋅ THENA Auto))
   THEN ((Assert CompFun((A)p) ∈ G.Equiv(decode(A);decode(B)) +⊢ Compositon((decode(A))p) BY
                ((RWW "csm-universe-decode" 0 THENA Auto)
                 THEN MemCD
                 THEN Repeat (BLemma `cubical-universe-p`)
                 THEN Auto))
         THEN (Assert CompFun((B)p) ∈ G.Equiv(decode(A);decode(B)) +⊢ Compositon((decode(B))p) BY
                     ((RWW "csm-universe-decode" 0 THENA Auto)
                      THEN MemCD
                      THEN Repeat (BLemma `cubical-universe-p`)
                      THEN Auto))
         )
   THEN (InstHyp [⌜A⌝] (-3)⋅ THENA Auto)
   THEN (D -4 With ⌜B⌝  THENA Auto)) }

1
1. [G] : CubicalSet{j}
2. [A] : {G ⊢ _:c𝕌}
3. [B] : {G ⊢ _:c𝕌}
4. G ⊢ decode(A)
5. (A)p ∈ {G.decode(A) ⊢ _:c𝕌}
6. G ⊢ decode(B)
7. (B)p ∈ {G.decode(A) ⊢ _:c𝕌}
8. G ⊢ Equiv(decode(A);decode(B))
9. G.decode(A) ⊢ Equiv((decode(A))p;(decode(B))p)
10. ∀[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)
11. (q)p ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((Equiv(decode(A);decode(B)))p)p}
12. (q)p ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:Equiv(((decode(A))p)p;((decode(B))p)p)}
13. equiv-fun((q)p) ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:(((decode(A))p)p ⟶ ((decode(B))p)p)}
14. app(equiv-fun((q)p); q) ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((decode(B))p)p}
15. CompFun((A)p) ∈ G.Equiv(decode(A);decode(B)) +⊢ Compositon((decode(A))p)
16. CompFun((B)p) ∈ G.Equiv(decode(A);decode(B)) +⊢ Compositon((decode(B))p)
17. (A)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
18. (B)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
⊢ uabeta(G;A;B) ∈ {G ⊢ _:ΠEquiv(decode(A);decode(B)) Π(decode(A))p (Path_((decode(B))p)p
                                                                         app(PathTransport(app(UA; (q)p)); q)
                                                                         app(equiv-fun((q)p); q))}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G  \mvdash{}  \_:c\mBbbU{}\}].    (uabeta(G;A;B)  \mmember{}  \{G  \mvdash{}  \_:uabeta-type(G;A;B)\})


By

---

Latex:
((Intros\mcdot{}
    THEN  (Assert  G  \mvdash{}  decode(A)  BY
                            Auto)
    THEN  (Assert  (A)p  \mmember{}  \{G.decode(A)  \mvdash{}  \_:c\mBbbU{}\}  BY
                            (BLemma  `csm-ap-term-universe`  THEN  Auto))
    THEN  (Assert  G  \mvdash{}  decode(B)  BY
                            Auto)
    THEN  (Assert  (B)p  \mmember{}  \{G.decode(A)  \mvdash{}  \_:c\mBbbU{}\}  BY
                            (BLemma  `csm-ap-term-universe`  THEN  Auto))
    THEN  (Assert  G  \mvdash{}  Equiv(decode(A);decode(B))  BY
                            Auto)
    THEN  (Assert  G.decode(A)  \mvdash{}  Equiv((decode(A))p;(decode(B))p)  BY
                            (RWO  "csm-universe-decode"  0  THEN  Auto)))
  THEN  Unfold  `uabeta-type`  0
  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  EqCDA
                            THEN  InstLemmaIJ  `cubical-equiv-p`  []
                            THEN  RWW  "-1<"  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
                            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)
              THEN  (InstLemmaIJ  `csm-ap-term-universe`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}G.Equiv(decode(A);decode(B))\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}
                          THENA  Auto
                          ))
  THEN  ((Assert  CompFun((A)p)  \mmember{}  G.Equiv(decode(A);decode(B))  +\mvdash{}  Compositon((decode(A))p)  BY
                            ((RWW  "csm-universe-decode"  0  THENA  Auto)
                              THEN  MemCD
                              THEN  Repeat  (BLemma  `cubical-universe-p`)
                              THEN  Auto))
              THEN  (Assert  CompFun((B)p)  \mmember{}  G.Equiv(decode(A);decode(B))  +\mvdash{}  Compositon((decode(B))p)  BY
                                      ((RWW  "csm-universe-decode"  0  THENA  Auto)
                                        THEN  MemCD
                                        THEN  Repeat  (BLemma  `cubical-universe-p`)
                                        THEN  Auto))
              )
  THEN  (InstHyp  [\mkleeneopen{}A\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  (D  -4  With  \mkleeneopen{}B\mkleeneclose{}    THENA  Auto))

---

Home Index