---

Step * of Lemma transEquiv_wf

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _:c𝕌}]. ∀[p:{G ⊢ _:(Path_c𝕌 A B)}].  (transEquiv{i:l}(G;A;p) ∈ {G ⊢ _:Equiv(decode(A);decode(B))})
BY
{ ((Intros⋅
    THEN (InstLemma `cc-snd_wf` [⌜parm{j}⌝;⌜parm{i'}⌝;⌜G⌝;⌜c𝕌⌝]⋅ THENA Auto)
    THEN (RWO "csm-cubical-universe" (-1) THENA Auto)
    THEN (InstLemma `csm-ap-term-universe` [⌜parm{[i' | j]}⌝; ⌜parm{i}⌝;⌜G⌝;⌜G.c𝕌⌝;⌜p⌝;⌜A⌝]⋅ THENA Auto)
    THEN (Assert equivTerm(G.c𝕌;(A)p;q) ∈ {G.c𝕌 ⊢ _:(c𝕌)p} BY
                (RWO "csm-cubical-universe" 0 THEN Auto))
    THEN (Assert cubical-lam(G;equivTerm(G.c𝕌;(A)p;q)) ∈ {G ⊢ _:(c𝕌 ⟶ c𝕌)} BY
                (InstLemma `cubical-lam_wf` [⌜parm{j}⌝;⌜parm{i'}⌝]⋅ THEN BHyp -1 THEN Auto)))
   THEN (InstLemma `cubical-subst_wf` [⌜G⌝;⌜c𝕌⌝;⌜A⌝;⌜B⌝;⌜p⌝;⌜cubical-lam(G;equivTerm(G.c𝕌;(A)p;q))⌝]⋅ THENA Auto)
   THEN Assert ⌜∀B:{G ⊢ _:c𝕌}
                  (decode(app(cubical-lam(G;equivTerm(G.c𝕌;(A)p;q)); B)) = Equiv(decode(A);decode(B)) ∈ {G ⊢ _})⌝⋅) }

1
.....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 ⊢ _})

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 ⊢ _})
⊢ transEquiv{i:l}(G;A;p) ∈ {G ⊢ _:Equiv(decode(A);decode(B))}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G  \mvdash{}  \_:c\mBbbU{}\}].  \mforall{}[p:\{G  \mvdash{}  \_:(Path\_c\mBbbU{}  A  B)\}].
    (transEquiv\{i:l\}(G;A;p)  \mmember{}  \{G  \mvdash{}  \_:Equiv(decode(A);decode(B))\})


By

---

Latex:
((Intros\mcdot{}
    THEN  (InstLemma  `cc-snd\_wf`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}c\mBbbU{}\mkleeneclose{}]\mcdot{}  THENA  Auto)
    THEN  (RWO  "csm-cubical-universe"  (-1)  THENA  Auto)
    THEN  (InstLemma  `csm-ap-term-universe`  [\mkleeneopen{}parm\{[i'  |  j]\}\mkleeneclose{};  \mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}G.c\mBbbU{}\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}
                THENA  Auto
                )
    THEN  (Assert  equivTerm(G.c\mBbbU{};(A)p;q)  \mmember{}  \{G.c\mBbbU{}  \mvdash{}  \_:(c\mBbbU{})p\}  BY
                            (RWO  "csm-cubical-universe"  0  THEN  Auto))
    THEN  (Assert  cubical-lam(G;equivTerm(G.c\mBbbU{};(A)p;q))  \mmember{}  \{G  \mvdash{}  \_:(c\mBbbU{}  {}\mrightarrow{}  c\mBbbU{})\}  BY
                            (InstLemma  `cubical-lam\_wf`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{}]\mcdot{}  THEN  BHyp  -1  THEN  Auto)))
  THEN  (InstLemma  `cubical-subst\_wf`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}c\mBbbU{}\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}cubical-lam(G;equivTerm(G.c\mBbbU{};(A)p;q))\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Assert  \mkleeneopen{}\mforall{}B:\{G  \mvdash{}  \_:c\mBbbU{}\}
                                (decode(app(cubical-lam(G;equivTerm(G.c\mBbbU{};(A)p;q));  B))
                                =  Equiv(decode(A);decode(B)))\mkleeneclose{}\mcdot{})

---

Home Index