The category of $π$-finite spaces
Mathieu Anel
TL;DR
The paper identifies the ∞-category S_π of π-finite spaces as a concrete, minimal higher analogue of finite sets that supports a broad suite of topos-like structures. It proves S_π is lex, extensive, exact, locally cartesian closed, and possesses a countable universe U_π in Spaces with a univalent family u_π, while also showing S_π is initial among ∞-pretopoi and initial among locally cartesian closed ∞-pretopoi with a Boolean subobject classifier. It also clarifies limitations: not all pushouts exist in S_π and there is no universe closed under all dependent sums/products, highlighting a fundamental distinction from elementary ∞-topoi. The work develops a robust toolkit (Simplicial/Segal groupoids, Kan resolutions, descent) to establish local cartesian closure and univalence in this setting, and provides an appendix tying univalent maps to pretopoi universes. Overall, it furnishes a concrete, initial, nontrivial model of a higher topos-like environment suitable for interpreting homotopy type theory while clarifying intrinsic higher-categorical constraints.
Abstract
We show that the category of truncated spaces with finite homotopy invariants ($π$\=/finite spaces) has many of the features expected of an elementary \oo topos. It should be thought of as the natural higher analogue of the elementary 1-topos of finite sets, with which it shares several initiality properties. The paper has also an appendix about univalent families in \oo pretopoi.