2025/04/30 by Martı́n Hötzel Escardó, Escardo, Martin, Alex Simpson +1
Computer Science · Mathematics · #Advanced Topology and Set Theory #Category Theory (math.CT) #FOS: Mathematics #General Topology (math.GN) #Homotopy and Cohomology in Algebraic Topology #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2504.21551
openalex publication_date 2025/04/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.