A 2-Sketchy Approach to Type Theory
Jonathan Osser

Abstract:
In this thesis we show how several of the common categorical structures for modeling type theory, comprehension categories and categories with families, can be given in terms of 2-dimensional limit theories and sketches. In order to have precise control over the homomorphisms, so that they align with those found in the literature, we take use finite limit F-theories and finite limit F-sketches as the notion of 2-dimensional theory. Using these tools, we show in detail how comprehension categories fit into the framework, with the weak maps matching the literature, and sketch how categories with families fit as well. We then show how to extend the theory for categories with families with several type constructors: dependent product types, dependent sum types, and extensional identity types. We show how the language of F-theories can be used to compare different models of type theory by showing the theory of categories with families equivalent to categories with attributes as F-categories, adapting the traditional proof. Finally, we show how this framework differs from earlier ones, Uemura’s categories with representable maps and Coraglia’s and Di Liberti’s judgemental theories, by modeling Gratzer’s multimode type theory, something which neither of the aforementioned frameworks can easily cover.