Displayed Monoidal Categories for the Semantics of Linear Logic
We present a formalization of different categorical structures used to interpret linear logic. Our formalization takes place in UniMath, a library of univalent mathematics based on the Coq proof assistant.
All the categorical structures we formalize are based on monoidal categories. As such, one of our contributions is a practical, usable library of formalized results on monoidal categories. Monoidal categories carry a lot of structure, and instances of monoidal categories are often built from complicated mathematical objects. This can cause challenges of scalability, regarding both the vast amount of data to be managed by the user of the library, as well as the time the proof assistant spends on checking code. To enable scalability, and to avoid duplication of computer code in the formalization, we develop “displayed monoidal categories”. These gadgets allow for the modular construction of complicated monoidal categories by building them in layers; we demonstrate their use in many examples. Specifically, we define linear-non-linear categories and construct instances of them via Lafont categories and linear categories.
Tue 16 JanDisplayed time zone: London change
11:00 - 12:30 | Formalizations of Category TheoryCPP at Kelvin Lecture Chair(s): Robert Atkey University of Strathclyde | ||
11:00 30mTalk | Displayed Monoidal Categories for the Semantics of Linear Logic CPP Benedikt Ahrens Delft University of Technology, Ralph Matthes IRIT, Université de Toulouse, CNRS, Toulouse INP, UT3, Toulouse, Niels van der Weide Radboud University, Kobe Wullaert Delft University of Technology | ||
11:30 30mTalk | Univalent Double Categories CPP Niels van der Weide Radboud University, Nima Rasekh Max Planck Institute for Mathematics, Benedikt Ahrens Delft University of Technology, Paige Randall North Utrecht University | ||
12:00 30mTalk | Formalizing the ∞-categorical Yoneda lemma CPP Nikolai Kudasov Innopolis University, Emily Riehl Johns Hopkins University, Jonathan Weinberger Johns Hopkins University Link to publication DOI Pre-print |