---

Step * 2 of Lemma transEquiv_wf


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))})
10. ∀B:{G ⊢ _:c𝕌}. (decode(app(cubical-lam(G;equivTerm(G.c𝕌;(A)p;q)); B)) = Equiv(decode(A);decode(B)) ∈ {G ⊢ _})
⊢ transEquiv{i:l}(G;A;p) ∈ {G ⊢ _:Equiv(decode(A);decode(B))}
BY
{ InstHyp [⌜IdEquiv(G;decode(A))⌝] (-2)⋅ }

1
.....wf..... 
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))})
10. ∀B:{G ⊢ _:c𝕌}. (decode(app(cubical-lam(G;equivTerm(G.c𝕌;(A)p;q)); B)) = Equiv(decode(A);decode(B)) ∈ {G ⊢ _})
⊢ IdEquiv(G;decode(A)) ∈ {G ⊢ _:decode(app(cubical-lam(G;equivTerm(G.c𝕌;(A)p;q)); A))}

2
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))})
10. ∀B:{G ⊢ _:c𝕌}. (decode(app(cubical-lam(G;equivTerm(G.c𝕌;(A)p;q)); B)) = Equiv(decode(A);decode(B)) ∈ {G ⊢ _})
11. cubical-subst(G;cubical-lam(G;equivTerm(G.c𝕌;(A)p;q));p;IdEquiv(G;decode(A)))
    ∈ {G ⊢ _:decode(app(cubical-lam(G;equivTerm(G.c𝕌;(A)p;q)); B))}
⊢ transEquiv{i:l}(G;A;p) ∈ {G ⊢ _:Equiv(decode(A);decode(B))}

---

Latex:

---

Latex:

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))\})
10.  \mforall{}B:\{G  \mvdash{}  \_:c\mBbbU{}\}
            (decode(app(cubical-lam(G;equivTerm(G.c\mBbbU{};(A)p;q));  B))  =  Equiv(decode(A);decode(B)))
\mvdash{}  transEquiv\{i:l\}(G;A;p)  \mmember{}  \{G  \mvdash{}  \_:Equiv(decode(A);decode(B))\}


By

---

Latex:
InstHyp  [\mkleeneopen{}IdEquiv(G;decode(A))\mkleeneclose{}]  (-2)\mcdot{}

---

Home Index