---

Step * 1 of Lemma app-univ-a


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𝕌)}
BY
{ ((Assert G ⊢ Equiv(decode(A);decode(B)) BY
          Auto)
   THEN ((InstLemmaIJ `csm-ap-term-universe` [⌜G⌝;⌜G.Equiv(decode(A);decode(B))⌝;⌜p⌝]⋅ THENA Auto)
         THEN (InstHyp [⌜A⌝] (-1)⋅ THENA Auto)
         THEN (D -2 With ⌜B⌝  THENA Auto))
   THEN (InstLemmaIJ `equiv_path_wf` [⌜G.Equiv(decode(A);decode(B))⌝;⌜(A)p⌝;⌜(A)p⌝]⋅ THENA Auto)
   THEN RepUR ``equiv-path term-to-path`` 0
   THEN (InstLemma `csm-cubical-lam`  [⌜parm{i|j}⌝;⌜parm{i'}⌝;⌜G.Equiv(decode(A);decode(B))⌝;⌜𝕀⌝;⌜c𝕌⌝]⋅ THENA 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𝕌)}
7. G ⊢ Equiv(decode(A);decode(B))
8. (A)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
9. (B)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
10. ∀[f:{G.Equiv(decode(A);decode(B)) ⊢ _:Equiv(decode((A)p);decode((A)p))}]
      (equiv_path(G.Equiv(decode(A);decode(B));(A)p;(A)p;f) ∈ {G.Equiv(decode(A);decode(B)).𝕀 ⊢ _:c𝕌})
11. ∀[b:{G.Equiv(decode(A);decode(B)).𝕀 ⊢ _:(c𝕌)p}]. ∀[H:ij⊢]. ∀[s:H ij⟶ G.Equiv(decode(A);decode(B))].
      ((cubical-lam(G.Equiv(decode(A);decode(B));b))s = cubical-lam(H;(b)s+) ∈ {H ⊢ _:((𝕀 ⟶ c𝕌))s})
⊢ ((λequiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))[f] = (λequiv_path(G;A;B;f)) ∈ {G ⊢ _:Path(c𝕌)}

---

Latex:

---

Latex:

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


By

---

Latex:
((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{}]\mcdot{}  THENA  Auto)
              THEN  (InstHyp  [\mkleeneopen{}A\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
              THEN  (D  -2  With  \mkleeneopen{}B\mkleeneclose{}    THENA  Auto))
  THEN  (InstLemmaIJ  `equiv\_path\_wf`  [\mkleeneopen{}G.Equiv(decode(A);decode(B))\mkleeneclose{};\mkleeneopen{}(A)p\mkleeneclose{};\mkleeneopen{}(A)p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``equiv-path  term-to-path``  0
  THEN  (InstLemma  `csm-cubical-lam` 
              [\mkleeneopen{}parm\{i|j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}G.Equiv(decode(A);decode(B))\mkleeneclose{};\mkleeneopen{}\mBbbI{}\mkleeneclose{};\mkleeneopen{}c\mBbbU{}\mkleeneclose{}]\mcdot{}
              THENA  Auto
              ))

---

Home Index