Sixteenth Annual IEEE Symposium on

Logic in Computer Science (LICS 2001)

Paper: A Universal Characterization of the Closed Euclidean Interval (at LICS 2001)

Authors: Martín H. Escardó Alex K. Simpson

Abstract

We propose a notion of interval object in a category with finite products, providing a universal property for closed and bounded real line segments. The universal property gives rise to an analogue of primitive recursion for defining computable functions on the interval. We use this to define basic arithmetic operations and to verify equations between them. We test the notion in categories of interest. In the category of sets, any closed and bounded interval of real numbers is an interval object. In the category of topological spaces, the interval objects are closed and bounded intervals with the Euclidean topology. We also prove that an interval object exists in any elementary topos with natural numbers object.

BibTeX

  @InProceedings{EscardSimpson-AUniversalCharacter,
    author = 	 {Martín H. Escardó and Alex K. Simpson},
    title = 	 {A Universal Characterization of the Closed Euclidean Interval},
    booktitle =  {Proceedings of the Sixteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2001},
    year =	 2001,
    editor =	 {Joseph Halpern},
    month =	 {June}, 
    pages =      {115--128},
    location =   {Boston, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }