---

Step * of Lemma univ-a_wf

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _:c𝕌}].  (UA ∈ {G ⊢ _:(Equiv(decode(A);decode(B)) ⟶ (Path_c𝕌 A B))})
BY
{ ( Intros⋅
   THEN Unhide
   THEN (Assert G ⊢ Equiv(decode(A);decode(B)) BY
               Auto)
   THEN ((InstLemmaIJ `csm-ap-term-universe`  [⌜G⌝;⌜G.Equiv(decode(A);decode(B))⌝;⌜p⌝;⌜A⌝]⋅ THENA Auto)
         THEN (InstLemmaIJ `csm-ap-term-universe`  [⌜G⌝;⌜G.Equiv(decode(A);decode(B))⌝;⌜p⌝;⌜B⌝]⋅ THENA Auto)
         )
   THEN Unfold `univ-a` 0
   THEN InstLemma `cubical-lam_wf` [parm{i|j};⌜parm{i'}⌝]⋅
   THEN (BHyp -1 THENL [Auto; Auto; Auto; InferEqualTypeGen])) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. G ⊢ Equiv(decode(A);decode(B))
5. (A)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
6. (B)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
7. ∀[X:ij⊢]. ∀[A,B:{X ⊢' _}]. ∀[b:{X.A ⊢ _:(B)p}].  (cubical-lam(X;b) ∈ {X ⊢ _:(A ⟶ B)})
⊢ {G.Equiv(decode(A);decode(B)) ⊢ _:(Path_c𝕌 (A)p (B)p)}
= {G.Equiv(decode(A);decode(B)) ⊢ _:((Path_c𝕌 A B))p}
∈ 𝕌{[i | [j | i]']}

2
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. G ⊢ Equiv(decode(A);decode(B))
5. (A)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
6. (B)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
7. ∀[X:ij⊢]. ∀[A,B:{X ⊢' _}]. ∀[b:{X.A ⊢ _:(B)p}].  (cubical-lam(X;b) ∈ {X ⊢ _:(A ⟶ B)})
8. {G.Equiv(decode(A);decode(B)) ⊢ _:(Path_c𝕌 (A)p (B)p)}
= {G.Equiv(decode(A);decode(B)) ⊢ _:((Path_c𝕌 A B))p}
∈ 𝕌{[i | [j | i]']}
⊢ EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q) ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:(Path_c𝕌 (A)p (B)p)}

---

Latex:

---

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


By

---

Latex:
(  Intros\mcdot{}
  THEN  Unhide
  THEN  (Assert  G  \mvdash{}  Equiv(decode(A);decode(B))  BY
                          Auto)
  THEN  ((InstLemmaIJ  `csm-ap-term-universe`
                  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}G.Equiv(decode(A);decode(B))\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}
                THENA  Auto
                )
              THEN  (InstLemmaIJ  `csm-ap-term-universe`
                            [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}G.Equiv(decode(A);decode(B))\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}
                          THENA  Auto
                          )
              )
  THEN  Unfold  `univ-a`  0
  THEN  InstLemma  `cubical-lam\_wf`  [parm\{i|j\};\mkleeneopen{}parm\{i'\}\mkleeneclose{}]\mcdot{}
  THEN  (BHyp  -1  THENL  [Auto;  Auto;  Auto;  InferEqualTypeGen]))

---

Home Index