The category of $\pi$-finite spaces

Abstract

We show that the category of truncated spaces with finite homotopy invariants ($\pi$\=/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.

v2. add an initiality result and the proof that not all pushout exist. v3 new appendix on univalent families in pretopoi and renew section on the universe of pi-finite spaces, corrected a few mistakes. v4 simplified a few proofs, last version before publication in JPAA