Logo

Mathematical Sciences Research Institute

Home » Homotopy Type Theory Electronic Seminar Talks: Univalence of the universal coCartesian fibration

Seminar

Homotopy Type Theory Electronic Seminar Talks: Univalence of the universal coCartesian fibration April 02, 2020 (08:30 AM PDT - 10:00 AM PDT)
Parent Program:
Location: MSRI: Online/Virtual
Speaker(s) Denis-Charles Cisinski (Universität Regensburg)
Description No Description
Video
No Video Uploaded
Abstract/Media

The model of higher categories given by Joyal's model structure for quasi-categories has univalent universes of coCartesian fibrations. This subsumes the existence of univalent universes of Kan fibrations proved by Voevodsky. Furthermore, the existence of such universes can be used as an alternative to the yoga of homotopy coherent nerves to prove all the essential features of higher category theory, giving a (directed) type theoretic approach to the foundations of higher categories.

 

https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html

No Notes/Supplements Uploaded No Video Files Uploaded