(For constructive purposes, take the strictest sense of ‘finite’.)
It is easy (and thus common) to make skeletal; there is one object for each natural number (including ), and a morphism from to is an -tuple of numbers satisfying . This amounts to identifying with the set . (Sometimes is used instead.)
The simplex category embeds into as a category with the same objects but fewer morphisms. The category of cyclic sets introduced by Connes lies in between. All the three are special cases of extensions of by a group in a particularly nice way. Full classification of allowed skew-simplicial sets has been given by Krasauskas and independently by Loday and Fiedorowicz.
The cartesian monoidal category of nonempty finite sets is the multi-sorted Lawvere theory of unbiased boolean algebras. As a lawvere theory, has one more sort, corresponding to , and one more model, in which every sort has exactly one element (in all the other models, the sort corresponding to is empty).
Mathematics done within or about is finite mathematics.
This is discussed for instance as (Awodey, prop. 7.31). For the generalization to all sets see at Set – Properties – Opposite category and Boolean algebras. See at Stone duality for more on this.
In constructive mathematics, for any flavor of finite, defines an equivalence of with the opposite category of that of those complete atomic Heyting algebras whose set of atomic elements is finite (in the same sense as in the definition of ).