Step
*
of Lemma
cubical-fst-at
∀[a,I,p:Top].  (p.1(a) ~ fst(p(a)))
BY
{ PresheafMLTTInstance Obid: presheaf-fst-at⋅ }
Latex:
Latex:
\mforall{}[a,I,p:Top].    (p.1(a)  \msim{}  fst(p(a)))
By
Latex:
PresheafMLTTInstance  Obid:  presheaf-fst-at\mcdot{}
Home
Index