---

Step * of Lemma constant-cubical-type-at

∀[X,I,a:Top].  ((X)(a) ~ X(I))
BY
{ PresheafMLTTInstance Obid: constant-presheaf-type-at⋅ }

---

Latex:

---

Latex:
\mforall{}[X,I,a:Top].    ((X)(a)  \msim{}  X(I))


By

---

Latex:
PresheafMLTTInstance  Obid:  constant-presheaf-type-at\mcdot{}

---

Home Index