---

Step * of Lemma univ-a_wf2

No Annotations
∀[G:j⊢]. (UA ∈ {G.c𝕌.c𝕌 ⊢ _:(Equiv(decode(q);decode((q)p)) ⟶ (Path_c𝕌 q (q)p))})
BY
{ ((Intros
    THEN (Assert q ∈ {G.c𝕌.c𝕌 ⊢ _:c𝕌} BY
                ((InstLemma `cc-snd_wf` [⌜parm{[i' | j]}⌝;⌜parm{i'}⌝;⌜G.c𝕌⌝;⌜c𝕌⌝]⋅ THENA Auto)
                 THEN RWO "csm-cubical-universe" (-1)
                 THEN Auto))
    )
   THEN (Assert q ∈ {G.c𝕌 ⊢ _:c𝕌} BY
               ((InstLemma `cc-snd_wf` [⌜parm{[i' | j]}⌝;⌜parm{i'}⌝;⌜G⌝;⌜c𝕌⌝]⋅ THENA Auto)
                THEN RWO "csm-cubical-universe" (-1)
                THEN Auto))
   THEN ((InstLemma `csm-ap-term_wf` [⌜parm{[i' | j]}⌝;⌜parm{i'}⌝;⌜G.c𝕌.c𝕌⌝;⌜G.c𝕌⌝;⌜c𝕌⌝;⌜p⌝;⌜q⌝]⋅ THENA Auto)
         THEN (RWO "csm-cubical-universe" (-1) THENA Auto)
         )
   THEN (InstLemma `univ-a_wf` [⌜parm{[i' | j]}⌝;⌜parm{i}⌝;⌜G.c𝕌.c𝕌⌝]⋅ THENA Auto)
   THEN BHyp -1
   THEN Try (Trivial)) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  (UA  \mmember{}  \{G.c\mBbbU{}.c\mBbbU{}  \mvdash{}  \_:(Equiv(decode(q);decode((q)p))  {}\mrightarrow{}  (Path\_c\mBbbU{}  q  (q)p))\})


By

---

Latex:
((Intros
    THEN  (Assert  q  \mmember{}  \{G.c\mBbbU{}.c\mBbbU{}  \mvdash{}  \_:c\mBbbU{}\}  BY
                            ((InstLemma  `cc-snd\_wf`  [\mkleeneopen{}parm\{[i'  |  j]\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}G.c\mBbbU{}\mkleeneclose{};\mkleeneopen{}c\mBbbU{}\mkleeneclose{}]\mcdot{}  THENA  Auto)
                              THEN  RWO  "csm-cubical-universe"  (-1)
                              THEN  Auto))
    )
  THEN  (Assert  q  \mmember{}  \{G.c\mBbbU{}  \mvdash{}  \_:c\mBbbU{}\}  BY
                          ((InstLemma  `cc-snd\_wf`  [\mkleeneopen{}parm\{[i'  |  j]\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}c\mBbbU{}\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  RWO  "csm-cubical-universe"  (-1)
                            THEN  Auto))
  THEN  ((InstLemma  `csm-ap-term\_wf`  [\mkleeneopen{}parm\{[i'  |  j]\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}G.c\mBbbU{}.c\mBbbU{}\mkleeneclose{};\mkleeneopen{}G.c\mBbbU{}\mkleeneclose{};\mkleeneopen{}c\mBbbU{}\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}
                THENA  Auto
                )
              THEN  (RWO  "csm-cubical-universe"  (-1)  THENA  Auto)
              )
  THEN  (InstLemma  `univ-a\_wf`  [\mkleeneopen{}parm\{[i'  |  j]\}\mkleeneclose{};\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}G.c\mBbbU{}.c\mBbbU{}\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  BHyp  -1
  THEN  Try  (Trivial))

---

Home Index