Project of the Applied Category Theory Adjoint School 2020
Mentor: Michael Shulman
TA: Paige Randall North
Project description
Type theories are formal systems allowing us to reason about categorical structures by “treating their objects as if they were sets” in a formal sense. While type theories for cartesian categorical structures are better-known, there are also “linear” type theories for non-cartesian structures. In this project we aim to construct a convenient type theory for reasoning about symmetric monoidal bicategories, which can be used to model many different kinds of open and interconnected systems. We will build on recent results establishing a similar type theory for symmetric monoidal categories as well as coherence theorems for symmetric monoidal bicategories.
Readings
- M. Shulman, A practical type theory for symmetric monoidal categories. arXiv:1911.00818
- Chris Schommer-Pries, The Classification of Two-Dimensional Extended Topological Field Theories, Chapter 2 only. arXiv:1112.1000v2