Euclidean interval objects in categories with finite products
Martin Escardo, Alex Simpson
TL;DR
This work provides a categorical, universal-property framework for interval objects in any category with finite products, unifying closed intervals across Sets, Top, and toposes without presupposing a real-number structure. Central to the construction are midpoint algebras, iteration via an infinitary operation, and the notion of m-convex bodies, which together yield a robust definition of an interval object as an initial, two-pointed, cancellative structure. In Sets, iterative midpoint objects coincide with iterative superconvex sets, enabling a concrete description of the free interval on two generators and a connection to simplices; in Top, the Euclidean interval with the standard topology realises the interval object via a continuous infinitary sum and magnifiability; and in elementary toposes with a natural numbers object, Euclidean-reals-based intervals provide interval objects, built through topos-internal Dedekind/Cauchy reals and fixed-point arguments. These results furnish a versatile tool for defining and manipulating interval-valued functions uniformly across diverse mathematical settings, with potential implications for computability, logic, and categorical geometry. The paper also establishes a detailed correspondence between iterative midpoint structures and iterative superconvex structures, yielding both conceptual clarity and practical constructions of interval-like objects in multiple categories.
Abstract
Based on the intuitive notion of convexity, we formulate a universal property defining interval objects in a category with finite products. Interval objects are structures corresponding to closed intervals of the real line, but their definition does not assume a pre-existing notion of real number. The universal property characterises such structures up to isomorphism, supports the definition of functions between intervals, and provides a means of verifying identities between functions. In the category of sets, the universal property characterises closed intervals of real numbers with nonempty interior. In the the category of topological spaces, we obtain intervals with the Euclidean topology. We also prove that every elementary topos with natural numbers object contains an interval object; furthermore, we characterise interval objects as intervals of real numbers in the Cauchy completion of the rational numbers within the Dedekind reals.