---

Step * 1 of Lemma app-univ-a-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)}
BY
{ ((InstLemmaIJ `equiv-path_wf` [⌜G.Equiv(decode(A);decode(B))⌝;⌜(A)p⌝;⌜(B)p⌝;⌜q⌝]⋅
    THENA (Auto THEN RWO "csm-universe-decode<" 0 THEN Auto)
    )
   THEN All (Unfold `cubical-lam`)
   THEN (InstLemma `cubical-beta` [⌜parm{j}⌝;⌜parm{i'}⌝;⌜G⌝;⌜Equiv(decode(A);decode(B))⌝]⋅ THENA Auto)) }

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}].  ((λb) ∈ {X ⊢ _:(A ⟶ B)})
9. EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q) ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:(Path_c𝕌 (A)p (B)p)}
10. ∀[B@0:{G.Equiv(decode(A);decode(B)) ⊢' _}]. ∀[b:{G.Equiv(decode(A);decode(B)) ⊢ _:B@0}].
    ∀[u:{G ⊢ _:Equiv(decode(A);decode(B))}].
      (app((λb); u) = (b)[u] ∈ {G ⊢ _:(B@0)[u]})
⊢ app((λ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:

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.  G  \mvdash{}  Equiv(decode(A);decode(B))
6.  (A)p  \mmember{}  \{G.Equiv(decode(A);decode(B))  \mvdash{}  \_:c\mBbbU{}\}
7.  (B)p  \mmember{}  \{G.Equiv(decode(A);decode(B))  \mvdash{}  \_:c\mBbbU{}\}
8.  \mforall{}[X:ij\mvdash{}].  \mforall{}[A,B:\{X  \mvdash{}'  \_\}].  \mforall{}[b:\{X.A  \mvdash{}  \_:(B)p\}].    (cubical-lam(X;b)  \mmember{}  \{X  \mvdash{}  \_:(A  {}\mrightarrow{}  B)\})
\mvdash{}  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]


By

---

Latex:
((InstLemmaIJ  `equiv-path\_wf`  [\mkleeneopen{}G.Equiv(decode(A);decode(B))\mkleeneclose{};\mkleeneopen{}(A)p\mkleeneclose{};\mkleeneopen{}(B)p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}
    THENA  (Auto  THEN  RWO  "csm-universe-decode<"  0  THEN  Auto)
    )
  THEN  All  (Unfold  `cubical-lam`)
  THEN  (InstLemma  `cubical-beta`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}Equiv(decode(A);decode(B))\mkleeneclose{}]\mcdot{}
              THENA  Auto
              ))

---

Home Index