Polynomials in homotopy type theory as a Kleisli category
Polynomials in homotopy type theory as a Kleisli category
Polynomials in a category have been studied as a generalization of the traditional notion in mathematics. Their construction has recently been extended to higher groupoids, as formalized in homotopy type theory, by Finster, Mimram, Lucas and Seiller, thus resulting in a cartesian closed bicategory. We refine and extend their work …