Andrew Swan: Introduction to cubical models of type theory

Abstract: The first cubical set model of type theory was introduced by Bezem, Coquand and Huber in order to provide a constructive model of homotopy type theory. Like the earlier, non-constructive simplicial set model due to Voevodsky it can be seen as based on ideas from homotopy theory and in particular Quillen model structures. However, for these ideas to work in constructive mathematics it was necessary to refine them carefully – definitions in homotopy theory that are easily equivalent with classical logic and the axiom of choice become distinct inside models of constructive mathematics, such as realizability models.

The aim of this talk is to give an introduction to cubical models of type theory, including motivation for using them, and some basic definitions and results to illustrate the overall idea.