Aspects of 2-categorical logic

Two ideas underpin categorical logic: first, that a theory can be identified with its associated syntactic category; secondly, that the set-theoretic models of a theory can be identified with functors from its syntactic category to the category of sets and functions preserving suitable structure. This point of view is useful because it often helps us to establish existence of free models. After reviewing these ideas, I will present joint work with Giacomo Tendas on variant in the context of 2-dimensional category theory, in which we are interested in categories, rather than sets, equipped with additional structure (often subject to universal properties). Extra subtleties emerge, as one needs to deal with a form of quantification in between `there exists’ and `there exists a unique’. As an application, we obtain a variety of free 2-categorical constructions, including Joyal’s free bicompletions.