Compact totally separated types
Abstract
Perhaps surprisingly, there are infinite types that can be exhaustively searched mechanically in finite time. We use ideas from topology to build plenty of them, referring to searchable types as compact types, and we use ordinals to measure their logical complexity. We consider two systems of ordinal notations under which a single notation denotes both a discrete ordinal and a compact one, with an embedding of the former into the latter whose image has empty complement. A boolean valued function decides which points in the image of the embedding are isolated and which are topological limit points. The first system consists of the traditional Brouwer codes and the second is an inductive-recursive universe generalizing them. The discrete ordinals so obtained are trichotomous, and the compact ones have the least element property for complemented subsets, but these two desirable properties cannot be fulfilled simultaneously in a constructive setting. The ordinals obtained from Brouwer codes further enjoy a boolean Leibniz principle, which has the notion of total separatedness as its topological counterpart. This extends previous work from Gödel's system T to intensional Martin-Löf type theory with univalent universes, and is formalized in Agda in the TypeTopology repository.
Related
- Quasi-isometries between graphs of totally disconnected locally compact groups
- The addition on totally positive integers uniquely determines the totally real number field
- Totally nonnegative tropical flags and the totally nonnegative flag Dressian
- On totally c-symplectically aspherical manifolds
- Totally invariant subvarieties of Pn
BibTeX
@misc{escardo2026compact,
title = {{Compact totally separated types}},
author = {Martín Hötzel Escardó},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.10447},
eprint = {2609.10447},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.10447},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Compact totally separated types
AU - Martín Hötzel Escardó
PY - 2026
DA - 2026/09/28
PB - arXiv
DO - 10.48550/arxiv.2609.10447
UR - https://arxiv.org/abs/2609.10447
AB - Perhaps surprisingly, there are infinite types that can be exhaustively searched mechanically in finite time. We use ideas from topology to build plenty of them, referring to searchable types as compact types, and we use ordinals to measure their logical complexity. We consider two systems of ordinal notations under which a single notation denotes both a discrete ordinal and a compact one, with an embedding of the former into the latter whose image has empty complement. A boolean valued function decides which points in the image of the embedding are isolated and which are topological limit points. The first system consists of the traditional Brouwer codes and the second is an inductive-recursive universe generalizing them. The discrete ordinals so obtained are trichotomous, and the compact ones have the least element property for complemented subsets, but these two desirable properties cannot be fulfilled simultaneously in a constructive setting. The ordinals obtained from Brouwer codes further enjoy a boolean Leibniz principle, which has the notion of total separatedness as its topological counterpart. This extends previous work from Gödel's system T to intensional Martin-Löf type theory with univalent universes, and is formalized in Agda in the TypeTopology repository.
ER -