---

Step * 1 1 of Lemma path-term-case1


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}
BY
{ (InstLemma `cubical-path-app_wf` [⌜X, psi⌝;⌜T⌝;⌜a⌝;⌜b⌝;⌜w⌝;⌜r⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

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)\}
8.  w  \mmember{}  \{X,  psi  \mvdash{}  \_:(Path\_T  a  b)\}
\mvdash{}  w  @  r  \mmember{}  \{X,  psi  \mvdash{}  \_:T\}


By

---

Latex:
(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)

---

Home Index