---

Step * 1 of Lemma path-trans_wf


1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. p : {G ⊢ _:(Path_c𝕌 A B)}
⊢ {G ⊢ _:((decode(path-eta(p)))[0(𝕀)] ⟶ (decode(path-eta(p)))[1(𝕀)])} = {G ⊢ _:(decode(A) ⟶ decode(B))} ∈ 𝕌{[i | j']}
BY
{ (RepeatFor 2 (EqCDA) THEN (RWO "csm-universe-decode" 0 THENA Auto) THEN (RWW "path-eta-0 path-eta-1" 0 THENA Auto)) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. p : {G ⊢ _:(Path_c𝕌 A B)}
⊢ decode(p @ 0(𝕀)) = decode(A) ∈ {G ⊢ _}

2
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. p : {G ⊢ _:(Path_c𝕌 A B)}
⊢ decode(p @ 1(𝕀)) = decode(B) ∈ {G ⊢ _}

---

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


By

---

Latex:
(RepeatFor  2  (EqCDA)
  THEN  (RWO  "csm-universe-decode"  0  THENA  Auto)
  THEN  (RWW  "path-eta-0  path-eta-1"  0  THENA  Auto))

---

Home Index