Français
On the ∞-topos semantics of homotopy type theory 1:
a categorical semantics of dependent type theory
Multi angle
Authors : Riehl, Emily (Author of the conference)
CIRM (Publisher )
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
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 : Keywords : homotopy type theory; infinity-topoi; categorical semantics
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, GuillaumeLanguage : English Available date : 14/03/2022 Conference Date : 21/02/2022 Subseries : Research School arXiv category : Logic ; Algebraic Topology Mathematical Area(s) : Logic and Foundations ; Topology Format : MP4 (.mp4) - HD Video Time : 01:33:58 Targeted Audience : Researchers ; Doctoral Students, Post-Doctoral Students Download : https://videos.cirm-math.fr/2022-02-21_Riehl_Part1.mp4 
|
Information on the Event
Event Title : Logic and higher structures / Logique et structures supérieuresEvent 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.19889603Cite this video as: 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 |
See Also
- [Multi angle] On the ∞-topos semantics of homotopy type theory 3: all ∞-toposes have strict univalent universes / Author of the conference Riehl, Emily.
- [Multi angle] On the ∞-topos semantics of homotopy type theory 2: the simplicial model of univalent foundations / Author of the conference Riehl, Emily.
- [Multi angle] Daily applications of the univalence axiom: lecture 3 / Author of the conference Rijke, Egbert.
- [Multi angle] Daily applications of the univalence axiom: lecture 2 / Author of the conference Rijke, Egbert.
- [Multi angle] Daily applications of the univalence axiom: lecture 1 / Author of the conference Rijke, Egbert.
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
