One notable shortcoming of standard semantics of type theory, such as categories with families (CwFs), is that each new type- and term- former must be introduced alongside laws stipulating that it is stable under substitution. When trying to give semantics for fully-featured type theories, such as Homotopy Type Theory, this can become quite tedious. This shortcoming can be overcome by working in a higher-order abstract syntax, which encodes variable binding as metatheoretic functions and makes stability under substitution implicit. Moreover, higher-order abstract syntax can be given semantics in presheaf categories [Hofmann 1999], whose category-theoretic properties are well-understood. Such approaches have recently been the focus of investigation in the form of second-order generalized algebraic theories, or SOGATs [Uemura 2019; Bocquet, et al. 2023], and in the development of higher observational type theory [Shulman 2022; Altenkirch, et al. 2024].

However, higher-order abstract syntax works by ‘abstracting’ away from explicit reference to contexts and substitutions. This means it is not obvious how to deploy these tools in the study of type theories with ‘modalities’, that is, explicit operations on contexts. This includes, for example, many varieties of directed type theory (e.g. [Harper and Licata 2011]) and modal type theory [Gratzer, et al. 2020]. In this talk, I describe some of my recent work (joint with Thorsten Altenkirch) to address this concern. In particular, I’ll discuss the category model of directed type theory (which is the directed analogue of the groupoid model of type theory [Hofmann and Streicher 1995]) and show how its two key modalities—opposite and core—can be made “abstract enough” to be expressible in higher-order abstract syntax. This will hopefully provide a roadmap for doing the same for arbitrary modalities, permitting us to combine these two exciting avenues of research.