Skip to main content

Anders Mörtberg: Constructive Presheaf Models of HoTT/UF

Time: Wed 2020-02-05 10.00 - 11.45

Lecturer: Anders Mörtberg

Location: Kräftriket, house 5, room 16


In recent years a variety of constructive presheaf models of Homotopy Type Theory and Univalent Foundations have been found. I will give an overview of these models and discuss some of the ideas that go into constructing them. A key idea of Ian Orton and Andrew Pitts is to axiomatize the models in the internal language of the presheaf topos and a variety of axiomatizations leading to different models have been found. These axioms are satisfied by any presheaf category where the base category has finite products and the interval object is representable, in particular by various cubical set categories. The talk will closely follow a recent survey article of Thierry Coquand titled “A survey of constructive presheaf models of univalence” that can be found at doi:10.1145/3242953.3242962

Belongs to: Department of Mathematics
Last changed: Jan 31, 2020