Français
On the ∞-topos semantics of homotopy type theory 2: the simplicial model of univalent foundations
Multi angle
Authors : ... (Author of the conference)
... (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
... (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
Language : EnglishAvailable date : 14/03/2022 Conference Date : 22/02/2022 Subseries : Research School arXiv category : Logic ; Algebraic Topology ; Algebraic Geometry Mathematical Area(s) : Logic and Foundations ; Topology Format : MP4 (.mp4) - HD Video Time : 01:21:55 Targeted Audience : Researchers ; Doctoral Students, Post-Doctoral Students Download : https://videos.cirm-math.fr/2022-02-22_Riehl_Part2.mp4 
|
Information on the Event
Event Title : Logic and higher structures / Logique et structures supérieuresDates : 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.19889903Cite this video as: (2022). On the ∞-topos semantics of homotopy type theory 2: the simplicial model of univalent foundations. CIRM. Audiovisual resource. doi:10.24350/CIRM.V.19889903 URI : http://dx.doi.org/10.24350/CIRM.V.19889903 |
See Also
- [Multi angle] On the ∞-topos semantics of homotopy type theory 3: all ∞-toposes have strict univalent universes / Author of the conference ....
- [Multi angle] On the ∞-topos semantics of homotopy type theory 1: - a categorical semantics of dependent type theory / Author of the conference ....
- [Multi angle] Daily applications of the univalence axiom: lecture 3 / Author of the conference ....
- [Multi angle] Daily applications of the univalence axiom: lecture 2 / Author of the conference ....
- [Multi angle] Daily applications of the univalence axiom: lecture 1 / Author of the conference ....
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
