A universal characterization of the unit interval

[Martin Escardo <m.escardo@cs.bham.ac.uk>]

The following extended abstract is now available on the Web.


     A universal characterization of the closed Euclidean interval

  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.


     http://www.cs.bham.ac.uk/~mhe/papers/lics2001-revised.ps 

Best wishes,

Martin Escardo & Alex Simpson
--
P.s. A draft full version with proofs is available on-line at

  http://www.dcs.ed.ac.uk/home/als/Research/interval.ps