---

Step * of Lemma sigma-unelim-p-type

∀[T:Top]. (((T)p)SigmaUnElim ~ ((T)p)p)
BY
{ PresheafMLTTInstance Obid: ps-sigma-unelim-p-type⋅ }

---

Latex:

---

Latex:
\mforall{}[T:Top].  (((T)p)SigmaUnElim  \msim{}  ((T)p)p)


By

---

Latex:
PresheafMLTTInstance  Obid:  ps-sigma-unelim-p-type\mcdot{}

---

Home Index