Martín Escardó: "Compact totally separated types in constructive univalent type theory"

Topos Institute Colloquium, 28th of April 2022. ——— If a type X is finite, then for every map p: X → 𝟚 we can tell, by exhaustive search, whether p has a root (we can exhibit x with p x = 0) or not (for every x : X we have that p x = 1). Perhaps surprisingly, there are infinite types X for which this decision is constructively possible. We call such types compact. It turns out that there are plenty of infinite compact types in any 1-topos. A basic, but perhaps surprising, example is the type ℕ∞ of decreasing infinite binary sequences. There are plenty more, and the purpose of this talk is to exhibit them. No matter how hard we tried to avoid that, all searchable types we could find happen to be well-ordered. But this is just as well, because we can use ordinals to measure how complicated the compact types that we can write down in constructive univalent type theory are. Much of the above discussion can be carried out in (the internal language of) a 1-topos. But then some of our constructions go beyond that, by considering the type of all ordinals in a universe, which is itself an ordinal in the next universe, and requires univalence and hence moves us to the realm of ∞-toposes. It remains to address the notion of total separatedness of a type X. This is the condition that there are plenty of maps X → 𝟚 to "separate the points of X" in a suitable sense. I'll rigorously define this and exhibit plenty of compact, totally separated, well-ordered types in univalent type theory. I will mention Johnstone's topological topos as an example of where "compact" and "totally separated" acquire their usual topological meaning. There is an old, non-constructive, theorem of topology that characterizes the compact countable Hausdorff spaces as the countable ordinals with the interval topology. In the topological topos, assuming a non-constructive meta-language to reason about it, the searchable objects we get are of this form.