---

Step * of Lemma formal-cube-restriction

∀[I,f,s,A,B:Top].  (f(s) ~ s ⋅ f)
BY
{ PresheafMLTTInstance2 Obid: Yoneda-restriction⋅ }

---

Latex:

---

Latex:
\mforall{}[I,f,s,A,B:Top].    (f(s)  \msim{}  s  \mcdot{}  f)


By

---

Latex:
PresheafMLTTInstance2  Obid:  Yoneda-restriction\mcdot{}

---

Home Index