---

Step * 1 of Lemma path-term-case1

.....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}
BY
{ ((Assert w ∈ {X, psi ⊢ _:(Path_T a b)} BY (SubsumeTT THEN BLemma `subset-cubical-term` THEN Auto)) THEN Unhide) }

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. w ∈ {X, psi ⊢ _:(Path_T a b)}
⊢ w @ r ∈ {X, psi ⊢ _:T}

---

Latex:

---

Latex:
.....wf..... 
1.  X  :  CubicalSet\{j\}
2.  psi  :  \{X  \mvdash{}  \_:\mBbbF{}\}
3.  r  :  \{X  \mvdash{}  \_:\mBbbI{}\}
4.  T  :  \{X  \mvdash{}  \_\}
5.  a  :  \{X  \mvdash{}  \_:T\}
6.  b  :  \{X  \mvdash{}  \_:T\}
7.  w  :  \{X,  psi  \mvdash{}  \_:(Path\_T  a  b)\}
\mvdash{}  w  @  r  \mmember{}  \{X,  psi  \mvdash{}  \_:T\}


By

---

Latex:
((Assert  w  \mmember{}  \{X,  psi  \mvdash{}  \_:(Path\_T  a  b)\}  BY
                (SubsumeTT  THEN  BLemma  `subset-cubical-term`  THEN  Auto))
  THEN  Unhide
  )

---

Home Index