---

Step * 1 of Lemma transEquiv_wf

.....assertion..... 
1. [G] : CubicalSet{j}
2. [A] : {G ⊢ _:c𝕌}
3. [B] : {G ⊢ _:c𝕌}
4. [p] : {G ⊢ _:(Path_c𝕌 A B)}
5. q ∈ {G.c𝕌 ⊢ _:c𝕌}
6. (A)p ∈ {G.c𝕌 ⊢ _:c𝕌}
7. equivTerm(G.c𝕌;(A)p;q) ∈ {G.c𝕌 ⊢ _:(c𝕌)p}
8. cubical-lam(G;equivTerm(G.c𝕌;(A)p;q)) ∈ {G ⊢ _:(c𝕌 ⟶ c𝕌)}
9. ∀[x:{G ⊢ _:decode(app(cubical-lam(G;equivTerm(G.c𝕌;(A)p;q)); A))}]
     (cubical-subst(G;cubical-lam(G;equivTerm(G.c𝕌;(A)p;q));p;x)
      ∈ {G ⊢ _:decode(app(cubical-lam(G;equivTerm(G.c𝕌;(A)p;q)); B))})
⊢ ∀B:{G ⊢ _:c𝕌}. (decode(app(cubical-lam(G;equivTerm(G.c𝕌;(A)p;q)); B)) = Equiv(decode(A);decode(B)) ∈ {G ⊢ _})
BY
{ Thin_andRename }

1
1. [G] : CubicalSet{j}
2. [A] : {G ⊢ _:c𝕌}
3. [B] : {G ⊢ _:c𝕌}
4. [p] : {G ⊢ _:(Path_c𝕌 A B)}
5. q ∈ {G.c𝕌 ⊢ _:c𝕌}
6. (A)p ∈ {G.c𝕌 ⊢ _:c𝕌}
7. equivTerm(G.c𝕌;(A)p;q) ∈ {G.c𝕌 ⊢ _:(c𝕌)p}
8. cubical-lam(G;equivTerm(G.c𝕌;(A)p;q)) ∈ {G ⊢ _:(c𝕌 ⟶ c𝕌)}
9. ∀[x:{G ⊢ _:decode(app(cubical-lam(G;equivTerm(G.c𝕌;(A)p;q)); A))}]
     (cubical-subst(G;cubical-lam(G;equivTerm(G.c𝕌;(A)p;q));p;x)
      ∈ {G ⊢ _:decode(app(cubical-lam(G;equivTerm(G.c𝕌;(A)p;q)); B))})
⊢ ∀B:{G ⊢ _:c𝕌}. (decode(app(cubical-lam(G;equivTerm(G.c𝕌;(A)p;q)); B)) = Equiv(decode(A);decode(B)) ∈ {G ⊢ _})

---

Latex:

---

Latex:
.....assertion..... 
1.  [G]  :  CubicalSet\{j\}
2.  [A]  :  \{G  \mvdash{}  \_:c\mBbbU{}\}
3.  [B]  :  \{G  \mvdash{}  \_:c\mBbbU{}\}
4.  [p]  :  \{G  \mvdash{}  \_:(Path\_c\mBbbU{}  A  B)\}
5.  q  \mmember{}  \{G.c\mBbbU{}  \mvdash{}  \_:c\mBbbU{}\}
6.  (A)p  \mmember{}  \{G.c\mBbbU{}  \mvdash{}  \_:c\mBbbU{}\}
7.  equivTerm(G.c\mBbbU{};(A)p;q)  \mmember{}  \{G.c\mBbbU{}  \mvdash{}  \_:(c\mBbbU{})p\}
8.  cubical-lam(G;equivTerm(G.c\mBbbU{};(A)p;q))  \mmember{}  \{G  \mvdash{}  \_:(c\mBbbU{}  {}\mrightarrow{}  c\mBbbU{})\}
9.  \mforall{}[x:\{G  \mvdash{}  \_:decode(app(cubical-lam(G;equivTerm(G.c\mBbbU{};(A)p;q));  A))\}]
          (cubical-subst(G;cubical-lam(G;equivTerm(G.c\mBbbU{};(A)p;q));p;x)
            \mmember{}  \{G  \mvdash{}  \_:decode(app(cubical-lam(G;equivTerm(G.c\mBbbU{};(A)p;q));  B))\})
\mvdash{}  \mforall{}B:\{G  \mvdash{}  \_:c\mBbbU{}\}
        (decode(app(cubical-lam(G;equivTerm(G.c\mBbbU{};(A)p;q));  B))  =  Equiv(decode(A);decode(B)))


By

---

Latex:
Thin\_andRename

---

Home Index