A uniform type theory for internal languages of categorical structures

Abstract

A hallmark of categorical logic is the interplay between category theory and type theory. A categorical structure can provide the semantics of a type theory; in the other direction, type theory can be used to describe the internal language of a categorical structure. The internal language is an ergonomic notation, based on elements and function application, to specify morphisms in the category. Typically, discovering an internal language is a bespoke process, performed anew for each categorical structure of interest. In this talk, we propose a uniform type theory giving internal languages for much of the “substructural” hierarchy of categorical logic, including such structures as categories, multicategories (planar, symmetric, and cartesian), PROPs, Lawvere theories, (symmetric) monoidal categories, cartesian categories, and Markov categories. The framework builds on the speaker’s work in double-categorical logic, and is described in preliminary form at: https://next.catcolab.org/rfc/0004