Fibred models of dual-context type theory and internal universes in models of HoTT

Add to your list(s) Download to your calendar using vCal

• Florrie Verity (Australian National University)
• Friday 26 September 2025, 14:00-15:00
• SS03, Computer Laboratory.

If you have a question about this talk, please contact Ioannis Markakis.

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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• Martin's interesting talks
• SS03, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• tcw57’s list
• yk373's list
• yk449

Note that ex-directory lists are not shown.