BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Fibred models of dual-context type theory and internal universes i
 n models of HoTT - Florrie Verity (Australian National University)
DTSTART:20250926T130000Z
DTEND:20250926T140000Z
UID:TALK236077@talks.cam.ac.uk
CONTACT:Ioannis Markakis
DESCRIPTION:The algebraic structures that feature in constructive\, preshe
 af-based models of homotopy type theory have been studied in two ways: usi
 ng the diagrammatic reasoning of category theory\, and by reasoning with j
 udgements in an internal type theory. These approaches are connected by th
 e standard semantics for extensional type theory\, and more recently\, by 
 a generalisation of Kripke-Joyal forcing semantics [1]. A notable exceptio
 n is the universal uniform fibration\, which cannot be expressed in the st
 andard 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-the
 oretic 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 d
 ual-context type theory\, show how it yields the appropriate internal lang
 uage\, and use this to give a precise correspondence between the two const
 ructions of the universal uniform fibration.\n\n\n[1] Steve Awodey\, Nicol
 a Gambino\, and Sina Hazratpour. Kripke-Joyal forcing for type theory and 
 uniform fibrations. Selecta Mathematica New Series\, 30(74)\, July 2024\n[
 2] Daniel R. Licata\, Ian Orton\, Andrew M. Pitts\, and Bas Spitters. Inte
 rnal universes in models of homotopy type theory. In Hélène Kirchner\, e
 ditor\, 3rd International Conference on Formal Structures for Computation 
 and Deduction (FSCD 2018)\, volume 108 of Leibniz International Proceeding
 s in Informatics (LIPIcs)\, pages 22:1–22:17\, Dagstuhl\, Germany\, 2018
 . 
LOCATION:SS03\, Computer Laboratory
END:VEVENT
END:VCALENDAR