---

Step * of Lemma presheaf-fst-at

∀[a,I,p:Top].  (p.1(a) ~ fst(p(a)))
BY
{ (RepUR ``presheaf-term-at presheaf-fst`` 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(RepUR  ``presheaf-term-at  presheaf-fst``  0  THEN  Auto)

---

Home Index