This talk is aimed at a general logic audience and will be presented at the British Logic Colloquium in September.

Homotopy Type Theory is a young area of logic building on connections between dependent type theory and algebraic topology. Its development began with studying models of type theory in settings richer than sets. The subsequent models of homotopy type theory have been studied in two ways: using the standard, diagrammatic reasoning of category theory, and using a logical style of reasoning via judgements in the “internal type theory” of a category. The latter technique has proved useful for managing structures that are otherwise diagrammatically complex.

To conveniently relate these two perspectives, Awodey, Gambino, and Hazratpour developed a generalisation of Kripke–Joyal forcing semantics and used it to prove properties of the algebraic structures that feature in models of homotopy type theory [1]. However, the standard internal type theory cannot express part of this structure, namely the “universal uniform fibration”. Its construction requires the type theory to be augmented with a modal operator restricting access to variables in the context [2]. As a result, to relate the category-theoretic and type-theoretic versions of the universal uniform fibration, we must first understand how to obtain this modal type theory as the internal language of a category. After laying out this problem, I will describe a solution and talk more broadly about the interest in modalities in the field of Homotopy Type Theory.

1. Steve Awodey, Nicola Gambino, and Sina Hazratpour. Kripke-Joyal forcing for type theory and uniform fibrations. Selecta Mathematica New Series, 30(74), July 2024
2. Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters. Internal universes in models of homotopy type theory. In Hélène Kirchner, editor, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), volume 108 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1–22:17, Dagstuhl, Germany, 2018. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.