---

Step * of Lemma app-univ-a-1

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _:c𝕌}]. ∀[f:{G ⊢ _:Equiv(decode(A);decode(B))}].
  (app(UA; f) = (EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))[f] ∈ {G ⊢ _:(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'}⌝]⋅) }

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G  \mvdash{}  \_:c\mBbbU{}\}].  \mforall{}[f:\{G  \mvdash{}  \_:Equiv(decode(A);decode(B))\}].
    (app(UA;  f)  =  (EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))[f])


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{})

---

Home Index