---

Step * of Lemma path-term-1

No Annotations
∀X:j⊢. ∀psi:{X ⊢ _:𝔽}. ∀T:{X ⊢ _}. ∀a,b:{X ⊢ _:T}. ∀w:{X, psi ⊢ _:(Path_T a b)}.
  (path-term(psi;w;a;b;1(𝕀)) = b ∈ {X ⊢ _:T})
BY
{ (Intros THEN RepUR ``path-term`` 0 THEN (InstLemma `cubical-path-app-1` [⌜X, psi⌝;⌜T⌝;⌜a⌝;⌜b⌝;⌜w⌝]⋅ THENA Auto)) }

1
1. X : CubicalSet{j}
2. psi : {X ⊢ _:𝔽}
3. T : {X ⊢ _}
4. a : {X ⊢ _:T}
5. b : {X ⊢ _:T}
6. w : {X, psi ⊢ _:(Path_T a b)}
7. w @ 1(𝕀) = b ∈ {X, psi ⊢ _:T}
⊢ (w @ 1(𝕀) ∨ (a ∨ b)) = b ∈ {X ⊢ _:T}

---

Latex:

---

Latex:
No  Annotations
\mforall{}X:j\mvdash{}.  \mforall{}psi:\{X  \mvdash{}  \_:\mBbbF{}\}.  \mforall{}T:\{X  \mvdash{}  \_\}.  \mforall{}a,b:\{X  \mvdash{}  \_:T\}.  \mforall{}w:\{X,  psi  \mvdash{}  \_:(Path\_T  a  b)\}.
    (path-term(psi;w;a;b;1(\mBbbI{}))  =  b)


By

---

Latex:
(Intros
  THEN  RepUR  ``path-term``  0
  THEN  (InstLemma  `cubical-path-app-1`  [\mkleeneopen{}X,  psi\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index