Step
*
of Lemma
formal-cube-is-rep-pre-sheaf
∀[I:Top]. (formal-cube(I) ~ rep-pre-sheaf(CubeCat;I))
BY
{ PresheafMLTTInstance2 Obid: Yoneda-is-rep-pre-sheaf⋅ }
Latex:
Latex:
\mforall{}[I:Top].  (formal-cube(I)  \msim{}  rep-pre-sheaf(CubeCat;I))
By
Latex:
PresheafMLTTInstance2  Obid:  Yoneda-is-rep-pre-sheaf\mcdot{}
Home
Index