---

Step * of Lemma path-term-case1

No Annotations
∀X:j⊢. ∀psi:{X ⊢ _:𝔽}.
  ∀[r:{X ⊢ _:𝕀}]
    ∀T:{X ⊢ _}. ∀a,b:{X ⊢ _:T}. ∀w:{X, psi ⊢ _:(Path_T a b)}.  (path-term(psi;w;a;b;r) = w @ r ∈ {X, psi ⊢ _:T})
BY
{ (Intros THEN Unfold `path-term` 0 THEN Fold `same-cubical-term` 0 THEN BLemma `case-term-equal-left` THEN Auto) }

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}X:j\mvdash{}.  \mforall{}psi:\{X  \mvdash{}  \_:\mBbbF{}\}.
    \mforall{}[r:\{X  \mvdash{}  \_:\mBbbI{}\}]
        \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;r)  =  w  @  r)


By

---

Latex:
(Intros
  THEN  Unfold  `path-term`  0
  THEN  Fold  `same-cubical-term`  0
  THEN  BLemma  `case-term-equal-left`
  THEN  Auto)

---

Home Index