The category of π-finite spaces

We show that the category of truncated spaces with finite homotopy invariants ( π -finite spaces) has many of the features expected of an elementary ∞-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 ∞-pretopoi.