En poursuivant votre navigation sur ce site, vous acceptez l'utilisation d'un simple cookie d'identification. Aucune autre exploitation n'est faite de ce cookie. OK
1

On the ∞-topos semantics of homotopy type theory 3: all ∞-toposes have strict univalent universes

Bookmarks Report an error
Multi angle
Authors : Riehl, Emily (Author of the conference)
CIRM (Publisher )

Loading the player...

Abstract : Many introductions to homotopy type theory and the univalence axiom neglect to explain what any of it means, glossing over the semantics of this new formal system in traditional set-based foundations. This series of talks will attempt to survey the state of the art, first presenting Voevodsky's simplicial model of univalent foundations and then touring Shulman's vast generalization, which provides an interpretation of homotopy type theory with strict univalent universes in any ∞-topos. As we will explain, this achievement was the product of a community effort to abstract and streamline the original arguments as well as develop new lines of reasoning.

Keywords : homotopy type theory; infinity-topoi; categorical semantics

MSC Codes :
03B38 - Type theory
18N60 - (∞,1)-categories (quasi-categories, Segal spaces, etc.); ∞-topoi, stable ∞-categories
18N40 - Homotopical algebra, Quillen model categories, derivators
18N50 - Simplicial sets, simplicial objects

Additional resources :
https://www.cirm-math.fr/RepOrga/2689/Notes/n_riehl_1.pdf

    Information on the Video

    Film maker : Hennenfent, Guillaume
    Language : English
    Available date : 14/03/2022
    Conference Date : 24/02/2022
    Subseries : Research School
    arXiv category : Logic ; Algebraic Topology
    Mathematical Area(s) : Logic and Foundations ; Topology
    Format : MP4 (.mp4) - HD
    Video Time : 01:40:57
    Targeted Audience : Researchers ; Doctoral Students, Post-Doctoral Students
    Download : https://videos.cirm-math.fr/2022-02-24_Riehl_Part3.mp4

Information on the Event

Event Title : Logic and higher structures / Logique et structures supérieures
Event Organizers : Ara, Dimitri ; Coquand, Thierry ; Mimram, Samuel
Dates : 21/02/2022 - 25/02/2022
Event Year : 2022
Event URL : https://conferences.cirm-math.fr/2689.html

Citation Data

DOI : 10.24350/CIRM.V.19890003
Cite this video as: Riehl, Emily (2022). On the ∞-topos semantics of homotopy type theory 3: all ∞-toposes have strict univalent universes. CIRM. Audiovisual resource. doi:10.24350/CIRM.V.19890003
URI : http://dx.doi.org/10.24350/CIRM.V.19890003

See Also

Bibliography

  • KAPULKIN, Chris et LUMSDAINE, Peter LeFanu. The simplicial model of univalent foundations (after Voevodsky). arXiv preprint arXiv:1211.2851, 2012. - https://arxiv.org/abs/1211.2851

  • SHULMAN, Michael. All $(\infty, 1) $-toposes have strict univalent universes. arXiv preprint arXiv:1904.07004, 2019. - https://arxiv.org/abs/1904.07004



Imagette Video

Bookmarks Report an error