A model of linear logic in homotopy type theory based on spans and polynomials


Elies Harington, Équipe Cosynus, laboratoire LIX, École Polytechnique. 24 avril 2025 10:00 TLR limd 2:00:00
Abstract:

Polynomial diagrams (also known as containers) are a categorification of the notion of polynomial. They can be defined in any category with pullbacks, where they form a bicategory. In the setting of homotopy type theory, we show that the (wild) category of polynomial diagrams in types can be recovered as a Kleisli category over the category of spans of types, thus fitting spans and polynomials respectively as the linear and non-linear part of a homotopical model of Linear Logic. If time allows, I will talk about how this fits in a framework of infinity-categorical models of Linear Logic that we are currently developing.