Recent developments in type theory have attempted to systematically recast properties of the syntax of a type theories (canonicity, normalization, etc.) into equivalent questions about the category of models. This dictionary relies on a formal link between the syntax of a theory and its category of models: the syntax of the theory must organize into an initial model. To expedite this process, several logical frameworks have been proposed which provide schemata for defining a type theory so that it automatically determines a category of models in which syntax is initial.

In this talk, rather than giving a new logical framework per se, we propose a new discipline for creating logical frameworks based around finitary 2-monads and sketches. As a case study of this approach, we show how locally Cartesian closed categories provide a suitable doctrine for type theories. We illustrate how a general theory of sketches [KPT99] can be used to define syntactic categories for type theories in a style that resembles the use of Martin-Löf's Logical Framework [NPS90], following the "judgments as types" principle [HHP93, ML87].

We prove a semantic adequacy result for locally Cartesian closed categories relative to Uemura's representable map categories [Uem19]: if a theory is definable in the framework of Uemura, the locally Cartesian closed category that it generates is a conservative (fully faithful) extension of its syntactic representable map category. On this basis, we argue for the use of locally Cartesian closed categories as a simpler alternative to Uemura's representable map categories.

This is joint work with Jonathan Sterling, and a preprint is available on arxiv: https://arxiv.org/abs/2012.10783