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 1:
a categorical semantics of dependent type theory

Sélection Signaler une erreur
Multi angle
Auteurs : Riehl, Emily (Auteur de la Conférence)
CIRM (Editeur )

Loading the player...

Résumé : 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

Codes MSC :
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

Ressources complémentaires :
https://www.cirm-math.fr/RepOrga/2689/Notes/n_riehl_1.pdf

    Informations sur la Vidéo

    Réalisateur : Hennenfent, Guillaume
    Langue : Anglais
    Date de publication : 14/03/2022
    Date de captation : 21/02/2022
    Sous collection : Research School
    arXiv category : Logic ; Algebraic Topology
    Domaine : Logic and Foundations ; Topology
    Format : MP4 (.mp4) - HD
    Durée : 01:33:58
    Audience : Researchers ; Doctoral Students, Post-Doctoral Students
    Download : https://videos.cirm-math.fr/2022-02-21_Riehl_Part1.mp4

Informations sur la Rencontre

Nom de la rencontre : Logic and higher structures / Logique et structures supérieures
Organisateurs de la rencontre : Ara, Dimitri ; Coquand, Thierry ; Mimram, Samuel
Dates : 21/02/2022 - 25/02/2022
Année de la rencontre : 2022
URL Congrès : https://conferences.cirm-math.fr/2689.html

Données de citation

DOI : 10.24350/CIRM.V.19889603
Citer cette vidéo: Riehl, Emily (2022). On the ∞-topos semantics of homotopy type theory 1:
a categorical semantics of dependent type theory. CIRM. Audiovisual resource. doi:10.24350/CIRM.V.19889603
URI : http://dx.doi.org/10.24350/CIRM.V.19889603

Voir aussi

Bibliographie

  • 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

Sélection Signaler une erreur