---

Step * of Lemma path-trans_wf

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _:c𝕌}]. ∀[p:{G ⊢ _:(Path_c𝕌 A B)}].  (PathTransport(p) ∈ {G ⊢ _:(decode(A) ⟶ decode(B))})
BY
{ (Auto THEN Unfold `path-trans` 0 THEN InferEqualTypeGen) }

1
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']}

2
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(𝕀)])}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G  \mvdash{}  \_:c\mBbbU{}\}].  \mforall{}[p:\{G  \mvdash{}  \_:(Path\_c\mBbbU{}  A  B)\}].
    (PathTransport(p)  \mmember{}  \{G  \mvdash{}  \_:(decode(A)  {}\mrightarrow{}  decode(B))\})


By

---

Latex:
(Auto  THEN  Unfold  `path-trans`  0  THEN  InferEqualTypeGen)

---

Home Index