Generalized point-free spaces, pointwise

TL;DR

This paper surveys the foundational principles of Grothendieck's generalized spaces, emphasizing a pointwise notation approach supported by known results, including applications in dependent type theory for bundles.

Contribution

It provides a comprehensive overview of generalized spaces with a focus on pointwise notation and clarifies conflicting terminologies in the field.

Findings

Supports a fully pointwise notation for generalized spaces.

Includes applications of dependent type theory to bundles.

Clarifies terminological conflicts in the literature.

Abstract

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.