The category of $\pi$-finite spaces

TL;DR

This paper explores the category of c0-finite spaces, demonstrating it shares many properties with an elementary  topos and serves as a higher analogue of finite sets, with implications for univalent families.

Contribution

It introduces and analyzes the category of c0-finite spaces, establishing its properties as a higher analogue of elementary 1-topos and discussing univalent families in
0 pretopoi.

Findings

c0-finite spaces form a category with topos-like features.

The category shares initiality properties with finite sets.

Includes an appendix on univalent families in
0 pretopoi.

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.