Abstract
In 2001 ([1]; but see [2] for a fuller version) Martín, together with Alex Simpson, gave a universal characterization of the closed Euclidean interval I = [-1, 1]. It addressed the problem of defining a path I → X between two given endpoints in X. We wish the path to be analogous to the straight line for the case where X is a real vector space, and obviously some structure on X is needed if this is to be defined; but it would be cheating just to require X to be a real vector space because we seek an independent characterization of the reals.
Martín and Alex identified the structure on X as being information to specify the midpoint of any two points of X, together with an “iterativity” condition. Then the characterization of I is that it is the free iterative midpoint algebra on two points (its endpoints).
They proved this for point-set versions of I, but they also conjectured it might hold point-free, and I proved this in [3]. I shall briefly outline my proof: it illustrates some features of the “ultraminimalist” geometric point-free reasoning that set it apart from other styles of constructive reasoning.
I shall follow by explaining how arcs on the circle can be proved to be iterative midpoint algebras, and this can then be used towards defining sin and cos by wrapping I around parts of the circle.
Talk Details
Speaker: Steve Vickers (University of Birmingham, UK)
Event: Types and Topology Workshop in Honour of Martin Escardo’s 60th Birthday
Date: Thursday 18 December 2025
Time: 11:35
Key Topics
- Escardó-Simpson interval objects
- Point-free topology
- Iterative midpoint algebras
- Constructive analysis
- Trigonometric functions
- Ultraminimalist geometric reasoning
- Circle geometry
- Path spaces
References
[1] M. Escardó and A. Simpson, A universal characterization of the closed Euclidean interval, in: Logic in Computer Science, 2001. Proceedings. 16th Annual IEEE Symposium on, (2001), pp. 115–125.
[2] M.H. Escardo and Alex K. Simpson. Euclidean interval objects in categories with finite products. arXiv:2504.21551, 30 Apr 2025.
[3] Steven Vickers “The localic compact interval is an Escardó-Simpson interval object”, Mathematical Logic Quarterly 63(6) (2017), pp. 614-629