If we were to characterize FinSet in terms of finite limits and colimits (and exponential objects) rather than just finite products and coproducts, then we could express both constraints and equivalences in the data types themselves. That in turn would allow us to write things like finite fields with their constraints in the type system itself, rather than postulating them as basic types (and thus having to figure out all the basic types that we need ahead of time). It would suffice for example to recursively include all of:
- Initial object
- Binary pushouts
- Terminal object
- Binary pullbacks
- Exponential objects
A system with recursive types would be definable by extending the introduction/elimination rules specified by the universal properties above with those of W-types built solely from the above, where W-types are specified as, for example, the initial algebras of functors defined as in polynomial functor in nLab (example code at geb/geb-idris/src/Library/IdrisCategories.idr at 7253188543c0839a0c428f11fd6978d54d945333 · anoma/geb · GitHub, doubtless among many other places), where the four objects and three morphisms involved all come only from FinSet. M-types (terminal coalgebras, i.e. not-necessarily-well-founded types such as streams) can also be defined in terms of those.