Polynomials in homotopy type theory as a Kleisli category

TL;DR

This paper extends the theory of polynomials in homotopy type theory, showing they form a Kleisli category equivalent to traditional polynomials, thus providing a homotopical model of linear logic.

Contribution

It generalizes the construction of polynomial categories in homotopy type theory and establishes their equivalence to classical polynomial categories, linking to linear logic models.

Findings

Polynomials form a Kleisli category equivalent to traditional polynomials.

Extended the free symmetric monoid monad to arbitrary universes.

Connected polynomial categories to models of linear logic.

Abstract

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 in multiple directions. We begin by generalizing the construction of the free symmetric monoid monad on types in order to handle arities in an arbitrary universe. Then, we extend this monad to the (wild) category of spans of types, and thus to a comonad by self-duality. Finally, we show that the resulting Kleisli category is equivalent to the traditional category of polynomials. This thus establishes polynomials as a (homotopical) model of linear logic. In fact, we explain that it is closely related to a bicategorical model of differential linear logic introduced by Melli\`es.