Abstract

The algebraic structures that feature in constructive, presheaf-based models of homotopy type theory have been studied in two ways: using the diagrammatic reasoning of category theory, and by reasoning with judgements in an internal type theory. These approaches are connected by the standard semantics for extensional type theory, and more recently, by a generalisation of Kripke-Joyal forcing semantics [1]. A notable exception is the universal uniform fibration, which cannot be expressed in the standard internal language of a presheaf category. Its construction requires extending the type theory with a modal operator, realised through a dual-context structure [2]. As a result, to precisely 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 an internal language of a category. In this talk, I will present a fibred model of dual-context type theory, show how it yields the appropriate internal language, and use this to give a precise correspondence between the two constructions of the universal uniform fibration.

[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.