---

Step * of Lemma ext-eq-cs_wf

No Annotations
∀[X,Y:j⊢].  (X ≡ Y ∈ ℙ{[i | j']})
BY
{ PresheafMLTTInstance Obid: ext-eq-psc_wf⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X,Y:j\mvdash{}].    (X  \mequiv{}  Y  \mmember{}  \mBbbP{}\{[i  |  j']\})


By

---

Latex:
PresheafMLTTInstance  Obid:  ext-eq-psc\_wf\mcdot{}

---

Home Index