  We survey foundational principles of Grothendieck's generalized spaces,
including a critical glossary of the various, and often conflicting,
terminological usages. Known results using generalized points support a fully
pointwise notation for these essentially point-free structures. This includes
some from dependent type theory to deal with bundles as continuous space-valued
maps, mapping base point to fibre.
