Home /  Cubical Sets (Part 1): The equivariant uniform Kan fibration model of cubical homotopy type theory

Seminar

Cubical Sets (Part 1): The equivariant uniform Kan fibration model of cubical homotopy type theory May 18, 2020 (01:00 PM PDT - 03:00 PM PDT)
Parent Program:
Location: SLMath: Online/Virtual
Speaker(s) Emily Riehl (Johns Hopkins University)
Description No Description
Keywords and Mathematics Subject Classification (MSC)
Primary Mathematics Subject Classification No Primary AMS MSC
Secondary Mathematics Subject Classification No Secondary AMS MSC
Video

The Equivariant Uniform Kan Fibration Model Of Cubical Homotopy Type Theory

Abstract/Media

Zoom Link:

https://msri.zoom.us/s/93059090699

 

In joint work with Steve Awodey, Evan Cavallo, Thierry Coquand, and Christian Sattler, we introduce a constructive model for homotopy type theory on a category of cubical sets that defines a model category that is Quillen equivalent to spaces and supports "cellularly-inductive" constructions. This latter property is a feature of the cube category we use: the cartesian cube category, which is an Eilenberg-Zilber generalized Reedy category. Our model is a variation of ABCFHL obtained by demanding that the fibrations satisfy an additional equivariance condition on top of the uniform Kan condition. As a consequence, all quotients of cubes by groups of symmetries are contractible. Time permitting, we sketch the proof of the comparison Quillen equivalence, which makes heavy use of these contractible cube quotients.

Asset no preview Notes 25.3 MB application/pdf

The Equivariant Uniform Kan Fibration Model Of Cubical Homotopy Type Theory

H.264 Video 25038_28427_8353_The_Equivariant_Uniform_Kan_Fibration_Model_of_Cubical_Homotopy_Type_Theory.mp4