---

Step * of Lemma app-univ-a

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _:c𝕌}]. ∀[f:{G ⊢ _:Equiv(decode(A);decode(B))}].
  (app(UA; f) = EquivPath(G;A;B;f) ∈ {G ⊢ _:(Path_c𝕌 A B)})
BY
{ (Intros⋅
   THEN (InstLemma `app-univ-a-1` [⌜G⌝;⌜A⌝;⌜B⌝;⌜f⌝]⋅ THENA Auto)
   THEN (Assert ⌜(EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))[f] = EquivPath(G;A;B;f) ∈ {G ⊢ _:(Path_c𝕌 A B)}⌝⋅
   THENM Auto
   )
   THEN (Assert EquivPath(G;A;B;f) ∈ {G ⊢ _:Path(c𝕌)} BY
               (SubsumeC ⌜{G ⊢ _:(Path_c𝕌 A B)}⌝⋅
                THEN Try ((InstLemma `path-type-sub-pathtype` [⌜parm{j}⌝;⌜parm{i'}⌝]⋅ THEN BHyp -1))
                THEN Auto))
   THEN (Enough to prove (EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))[f]
         = EquivPath(G;A;B;f)
         ∈ {G ⊢ _:Path(c𝕌)}
          Because (InstLemma `paths-equal` [⌜parm{j}⌝;⌜parm{i'}⌝]⋅ THEN BHyp -1 THEN Auto))) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. f : {G ⊢ _:Equiv(decode(A);decode(B))}
5. app(UA; f) = (EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))[f] ∈ {G ⊢ _:(Path_c𝕌 A B)}
6. EquivPath(G;A;B;f) ∈ {G ⊢ _:Path(c𝕌)}
⊢ (EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))[f] = EquivPath(G;A;B;f) ∈ {G ⊢ _:Path(c𝕌)}

---

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;A;B;f))


By

---

Latex:
(Intros\mcdot{}
  THEN  (InstLemma  `app-univ-a-1`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}(EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))[f]  =  EquivPath(G;A;B;f)\mkleeneclose{}\mcdot{}
  THENM  Auto
  )
  THEN  (Assert  EquivPath(G;A;B;f)  \mmember{}  \{G  \mvdash{}  \_:Path(c\mBbbU{})\}  BY
                          (SubsumeC  \mkleeneopen{}\{G  \mvdash{}  \_:(Path\_c\mBbbU{}  A  B)\}\mkleeneclose{}\mcdot{}
                            THEN  Try  ((InstLemma  `path-type-sub-pathtype`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{}]\mcdot{}  THEN  BHyp  -1))
                            THEN  Auto))
  THEN  (Enough  to  prove  (EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))[f]  =  EquivPath(G;A;B;f)
                Because  (InstLemma  `paths-equal`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{}]\mcdot{}  THEN  BHyp  -1  THEN  Auto)))

---

Home Index