Displayed Monoidal Categories for the Semantics of Linear Logic

Explore a 30-minute conference talk from CPP 2024 that delves into the formalization of categorical structures used to interpret linear logic. Learn about the development of displayed monoidal categories as a solution to scalability challenges in formalizing complex mathematical objects. Discover how these structures enable modular construction of complicated monoidal categories and their application in defining linear-non-linear categories. Gain insights into the formalization process using UniMath, a library of univalent mathematics based on the Coq proof assistant. Understand the practical implications of this work for creating usable libraries of formalized results on monoidal categories and their role in interpreting linear logic.