---

Step * 2 of Lemma path-trans_wf


1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. p : {G ⊢ _:(Path_c𝕌 A B)}
5. {G ⊢ _:((decode(path-eta(p)))[0(𝕀)] ⟶ (decode(path-eta(p)))[1(𝕀)])} = {G ⊢ _:(decode(A) ⟶ decode(B))} ∈ 𝕌{[i | j']}
⊢ univ-trans(G;path-eta(p)) ∈ {G ⊢ _:((decode(path-eta(p)))[0(𝕀)] ⟶ (decode(path-eta(p)))[1(𝕀)])}
BY
{ (Assert path-eta(p) ∈ {G.𝕀 ⊢ _:c𝕌} BY
         ((Assert {G ⊢ _:(Path_c𝕌 A B)} ⊆r {G ⊢ _:Path(c𝕌)} BY
                 (InstLemma `path-type-subtype` [⌜parm{j}⌝;⌜parm{i'}⌝]⋅ THEN BHyp -1 THEN Auto))
          THEN (InstLemma `path-eta_wf` [⌜parm{j}⌝;⌜parm{i'}⌝;⌜G⌝;⌜c𝕌⌝;⌜p⌝]⋅ THENA Auto)
          THEN RWO  "csm-cubical-universe" (-1)
          THEN Auto)) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. p : {G ⊢ _:(Path_c𝕌 A B)}
5. {G ⊢ _:((decode(path-eta(p)))[0(𝕀)] ⟶ (decode(path-eta(p)))[1(𝕀)])} = {G ⊢ _:(decode(A) ⟶ decode(B))} ∈ 𝕌{[i | j']}
6. path-eta(p) ∈ {G.𝕀 ⊢ _:c𝕌}
⊢ univ-trans(G;path-eta(p)) ∈ {G ⊢ _:((decode(path-eta(p)))[0(𝕀)] ⟶ (decode(path-eta(p)))[1(𝕀)])}

---

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.  \{G  \mvdash{}  \_:((decode(path-eta(p)))[0(\mBbbI{})]  {}\mrightarrow{}  (decode(path-eta(p)))[1(\mBbbI{})])\}
=  \{G  \mvdash{}  \_:(decode(A)  {}\mrightarrow{}  decode(B))\}
\mvdash{}  univ-trans(G;path-eta(p))  \mmember{}  \{G  \mvdash{}  \_:((decode(path-eta(p)))[0(\mBbbI{})]  {}\mrightarrow{}  (decode(path-eta(p)))[1(\mBbbI{})])\}


By

---

Latex:
(Assert  path-eta(p)  \mmember{}  \{G.\mBbbI{}  \mvdash{}  \_:c\mBbbU{}\}  BY
              ((Assert  \{G  \mvdash{}  \_:(Path\_c\mBbbU{}  A  B)\}  \msubseteq{}r  \{G  \mvdash{}  \_:Path(c\mBbbU{})\}  BY
                              (InstLemma  `path-type-subtype`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{}]\mcdot{}  THEN  BHyp  -1  THEN  Auto))
                THEN  (InstLemma  `path-eta\_wf`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}c\mBbbU{}\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  RWO    "csm-cubical-universe"  (-1)
                THEN  Auto))

---

Home Index