## Posts

### Extensional constructive real analysis via locators

This is an announcement of a paper in the areas of constructive mathematics, (univalent) type theory, and exact real arithmetic.

Abstract: Real numbers do not admit an extensional procedure for observing discrete information, such as the first digit of its decimal expansion, because every extensional, computable map from the reals to the integers is constant, as is well known. We overcome this by considering real numbers equipped with additional structure, which we call a locator. With this structure, it is possible, for instance, to construct a signed-digit representation or a Cauchy sequence, and conversely these intensional representations give rise to a locator. Although the constructions are reminiscent of computable analysis, instead of working with a notion of computability, we simply work constructively to extract observable information, and instead of working with representations, we consider a certain locatedness structure on real numbers.

To appear in the MSCS Special Issue …

### The HoTT book reals coincide with the Escardó-Simpson reals

This is an announcement of a paper in the area of univalent type theory and exact real arithmetic.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 notion of reals, and suggests that the interval 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 book reals is the least Cauchy complete subset of the Dedekind reals containing the rationals.
Preprint is on the arXiv.Somewhat stronger results can be found in Chapter 5 of my PhD thesis. I intend to publish these results at a later stage.

### Parametricity, automorphisms of the universe, and excluded middle

This is an announcement of a paper in the area of type theory and parametricity.

Specific violations of parametricity, or existence of non-identity automorphisms of the universe, can be used to prove classical axioms. The former was previously featured on the Homotopy Type Theory blog, and the latter is part of a discussion on the HoTT mailing list. In a cooperation between Martín Escardó, Peter Lumsdaine, Mike Shulman, and myself, we have strengthened these results and recorded them in a paper that is published in the post-proceedings of TYPES 2016 (see also the preprint on arXiv).