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

Tid: On 2020-02-05 kl 10.00 - 11.45

Föreläsare: Anders Mörtberg

Plats: Kräftriket, house 5, room 16

Abstract

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

Innehållsansvarig:webmaster@math.kth.se
Tillhör: Institutionen för matematik
Senast ändrad: 2020-01-31