Parametricity, Automorphisms of the Universe, and Excluded Middle. - Auke Bart Booij; Martín Hötzel Escardó; Peter LeFanu Lumsdaine; Michael Shulman (TYPES, 2016)

The HoTT reals coincide with the Escardó-Simpson reals. - Auke Bart Booij (CoRR, 2017)

Property and structure in constructive analysis. - Auke Bart Booij (CoRR, 2018)

Extensional constructive real analysis via locators. - Auke Bart Booij (Math. Struct. Comput. Sci., 2021)