Abstract
I will discuss how to define the signed digit reals à la Escardo/Simpson as a higher coinductive type. This is work in progress and I hope to get some input from Martin.
Talk Details
Speaker: Thorsten Altenkirch (University of Nottingham, UK)
Event: Types and Topology Workshop in Honour of Martin Escardo’s 60th Birthday
Date: Wednesday 17 December 2025
Time: 11:00
Slides: Available
Key Topics
- Higher coinductive types
- Signed digit reals
- Escardo/Simpson real number representation
- Coinduction in type theory
- Real number foundations
- Homotopy type theory
Related Work
- Steve Vickers - Escardó-Simpson interval objects and point-free trigonometry
- Alex Simpson - Martin’s interval in Scotland
- Escardo/Simpson work on real numbers
- Higher inductive-inductive types
Notes
This is presented as work in progress, with Altenkirch seeking input from Martin Escardó himself, highlighting the collaborative and ongoing nature of research in this area.