We extend homotopy type theory with four extra axioms. The resulting theory should describe the higher topos of light condensed sets. From the axioms, we can prove Markov’s principle, the lesser limited principle of omniscience, and the negation of the weak lesser principle of omniscience. We define a type of open propositions, which induces a topology on each type. With this topology, every map is continuous. We then introduce Stone and compact Hausdorff spaces internally, and the induced topologies on these types are as expected. In particular, we can deduce that all maps from the real unit interval to itself are continuous in the epsilon-delta sense.

This talk is based on a paper submitted to TYPES24, which was authored by Felix Cherubini, Thierry Coquand, Freek Geerligs and Hugo Moeneclaey. The paper is part of the synthetic algebraic geometry project.