Steve Awodey: Cubical Homotopy Type Theory

In this work-in-progress talk, I will analyse the cubical model of homotopy type theory of Coquand et al. in functorial terms, making a few modifications along the way.  The basic category of cubical sets used is presheaves on the free cartesian category on a bipointed object, i.e. the Lawvere theory of bipointed objects.  The presheaf category is the classifying topos for strictly bipointed objects.

The Kan extension property familiar from algebraic topology is shown to be exactly what is required to model the Identity-elimination rule of Martin-Löf, and the closure of Kan objects under function spaces is ensured constructively by Coquand’s uniformity condition, re-analysed as the existence of a certain natural transformation making natural choices of Kan fillers.  A universe of Kan objects is given in the style of the recent “natural models” construction, based on ideas of Lumsdaine-Warren and Voevodsky.