---

Step * of Lemma path-term-equal

No Annotations
∀X:j⊢. ∀psi:{X ⊢ _:𝔽}.
  ∀[r:{X ⊢ _:𝕀}]
    ∀T:{X ⊢ _}. ∀a,b:{X ⊢ _:T}. ∀w:{X, psi ⊢ _:(Path_T a b)}.
      ∀[z:{X ⊢ _:T}]
        path-term(psi;w;a;b;r) = z ∈ {X, (psi ∨ ((r=0) ∨ (r=1))) ⊢ _:T} 
        supposing (w @ r = z ∈ {X, psi ⊢ _:T}) ∧ (a = z ∈ {X, (r=0) ⊢ _:T}) ∧ (b = z ∈ {X, (r=1) ⊢ _:T})
BY
{ (RepeatFor 8 (Intro)
   THEN (Assert w @ r ∈ {X, psi ⊢ _:T} BY
               ((Assert w ∈ {X, psi ⊢ _:(Path_T a b)} BY
                       (SubsumeTT THEN BLemma `subset-cubical-term` THEN Auto))
                THEN Unhide
                THEN InstLemma `cubical-path-app_wf` [⌜X, psi⌝;⌜T⌝;⌜a⌝;⌜b⌝;⌜w⌝;⌜r⌝]⋅
                THEN Auto))
   THEN Intro) }

1
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. z : {X ⊢ _:T}
9. w @ r ∈ {X, psi ⊢ _:T}
10. (w @ r = z ∈ {X, psi ⊢ _:T}) ∧ (a = z ∈ {X, (r=0) ⊢ _:T}) ∧ (b = z ∈ {X, (r=1) ⊢ _:T})
⊢ path-term(psi;w;a;b;r) = z ∈ {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)\}.
            \mforall{}[z:\{X  \mvdash{}  \_:T\}].  path-term(psi;w;a;b;r)  =  z  supposing  (w  @  r  =  z)  \mwedge{}  (a  =  z)  \mwedge{}  (b  =  z)


By

---

Latex:
(RepeatFor  8  (Intro)
  THEN  (Assert  w  @  r  \mmember{}  \{X,  psi  \mvdash{}  \_:T\}  BY
                          ((Assert  w  \mmember{}  \{X,  psi  \mvdash{}  \_:(Path\_T  a  b)\}  BY
                                          (SubsumeTT  THEN  BLemma  `subset-cubical-term`  THEN  Auto))
                            THEN  Unhide
                            THEN  InstLemma  `cubical-path-app\_wf`  [\mkleeneopen{}X,  psi\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{}]\mcdot{}
                            THEN  Auto))
  THEN  Intro)

---

Home Index