Elies Harington ; Samuel Mimram - Polynomials in homotopy type theory as a Kleisli category

entics:14786 - Electronic Notes in Theoretical Informatics and Computer Science, December 11, 2024, Volume 4 - Proceedings of MFPS XL - https://doi.org/10.46298/entics.14786
Polynomials in homotopy type theory as a Kleisli categoryArticle

Authors: Elies Harington ; Samuel Mimram

    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ès.


    Volume: Volume 4 - Proceedings of MFPS XL
    Published on: December 11, 2024
    Accepted on: November 18, 2024
    Submitted on: November 18, 2024
    Keywords: Mathematics - Category Theory

    Consultation statistics

    This page has been seen 29 times.
    This article's PDF has been downloaded 9 times.