Starting from an ordinary 1-categorical point of view, there are various obvious candidate definitions for ‘finite homotopy type’:

- The homotopy type of a simplicial set that has only finitely many non-degenerate simplices.
- The homotopy type of a CW complex that has only finitely many cells.
- The homotopy type of the nerve of a finitely-presentable category.

Homotopy type theory affords another candidate:

- A higher inductive type that admits a finite presentation in some syntactic sense.

**Question.** Do these notions coincide? To what extent is each one the ‘right’ notion of finiteness for homotopy types? For instance, are these precisely the homotopy types $X$ such that the representable functor $\mathrm{Hom}(X, -) : \infty \mathbf{Grpd} \to \infty \mathbf{Grpd}$ preserves (homotopy) filtered colimits?