Polynomial Functors and W-Types in Groupoids
- Date: Wednesday 23 May 2018, 14:00 – 15:00
- Location: Mathematics Level 8, MALL 1, School of Mathematics
- Type: Proofs, Constructions and Computations, Seminars, Pure Mathematics
- Cost: Free
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.