2017/06/19 by Auke Bart Booij, Booij, Auke Bart · 1 voice
Computer Science · Mathematics · #Advanced Topology and Set Theory #Category Theory (math.CT) #Computability, Logic, AI Algorithms #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #Mathematical and Theoretical Analysis #cs.LO #math.CT #math.LO
paper · pdf · doi:10.48550/arxiv.1706.05956
openalex publication_date 2017/06/19 · arxiv published 2017/06/19 · openalex created_date 2025/10/10 · arxiv updated 2026/06/29 · openalex updated_date 2026/07/28
Escardó and Simpson defined a notion of interval object by a universal property in any category with binary products. The Homotopy Type Theory book defines a higher inductive-inductive notion of reals, and suggests that the interval in this type may satisfy this universal property. We show that this is indeed the case in the category of sets of any universe. We also show that the type of HoTT reals is the smallest Cauchy complete subset of the Dedekind reals containing the rationals.