A Cartesian Bicategory of Polynomial Functors in Homotopy Type Theory
A Cartesian Bicategory of Polynomial Functors in Homotopy Type Theory
Polynomial functors are a categorical generalization of the usual notion of polynomial, which has found many applications in higher categories and type theory: those are generated by polynomials consisting a set of monomials built from sets of variables. They can be organized into a cartesian bicategory, which unfortunately fails to …