---

Step * of Lemma path-term_wf

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) ∈ {X, (psi ∨ ((r=0) ∨ (r=1))) ⊢ _:T})
BY
{ (Intros THEN Assert ⌜a ∈ {X, (r=0) ⊢ _:T[(r=1) |⟶ b]}⌝⋅) }

1
.....assertion..... 
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)}
⊢ a ∈ {X, (r=0) ⊢ _:T[(r=1) |⟶ b]}

2
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)}
8. a ∈ {X, (r=0) ⊢ _:T[(r=1) |⟶ b]}
⊢ path-term(psi;w;a;b;r) ∈ {X, (psi ∨ ((r=0) ∨ (r=1))) ⊢ _: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)  \mmember{}  \{X,  (psi  \mvee{}  ((r=0)  \mvee{}  (r=1)))  \mvdash{}  \_:T\})


By

---

Latex:
(Intros  THEN  Assert  \mkleeneopen{}a  \mmember{}  \{X,  (r=0)  \mvdash{}  \_:T[(r=1)  |{}\mrightarrow{}  b]\}\mkleeneclose{}\mcdot{})

---

Home Index