Polynomial functors

A Cartesian Bicategory of Polynomial Functors in Homotopy Type Theory

We propose that the cartesian bicategory of polynomial functors, which unfortunately fails to be closed for essentially two reasons, can be addressed by suitably modifying the model.First, a naive closure is too large to be well-defined, which can be overcome by restricting to polynomials which are finitary.Second, the resulting putative closure fails to properly take the 2-categorical structure in account.We advocate here that this can be addressed by considering polynomials in groupoids, instead of sets.