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