Polynomial Functors and W-Types in Groupoids

Jakob Vidmar, University of Leeds. Part of the proofs, constructions and computations seminar series.

In type theory, W-types are types that are defined inductively, for example natural numbers, lists, trees and other well-founded data structures. Categorically we model this as initial algebras of polynomial functors in some locally closed Cartesian category. This was explored in the work of N. Gambino, M. Hyland, J. Kock, I. Moerdijk, etc.

Unfortunately, the category of groupoids in not locally Cartesian closed. However, some parts of the theory of polynomial functors and their initial algebras can be recovered. We will discuss some aspects of this and observe, on examples, what we obtain by generalising to the category of groupoids.