Reid W. Barton: Condensed type theory and directed univalence

Abstract

Many mathematical objects (such as the real numbers or p-adic numbers) come with a "natural" topology, traditionally thought of as additional structure on an underlying set. The category of condensed sets, introduced by Clausen and Scholze, is a close approximation to topological spaces with the advantage of being a topos, and therefore supporting a model of type theory. The type theoretic definitions of objects such as the real numbers then tend to produce these objects along with their expected topologies.

In this talk, I will describe a list of type-theoretic axioms satisfied by condensed sets along with two distinguished subuniverses, the "compact Hausdorff" and "overt discrete" types. From these axioms, it is possible to prove for example that every function from the Dedekind reals to itself is continuous in the standard sense. Perhaps a more surprising consequence is that the subuniverse ODisc of overt discrete types satisfies a form of directed univalence, which implies that every function from ODisc to itself is actually a functor.

This is joint work with Johan Commelin.