Mini-course: Cubical Type Theory
The cubical sets models of type theory by Bezem, Coquand, and Huber (2013), and Cohen, Coquand, Huber, and Mörtberg (2014-2015) are constructive interpretations of homotopy type theory. These models inspired a line of work on cubical type theories (by Cohen, Coquand, Huber, and Mörtberg; Brunerie, Licata, Angiuli, and Harper; Altenkirch and Kaposi; Polonsky), which take the extra structure present in these models and build it into the syntax of type theory in some way. Cubical techniques can also be simulated to some extent in "axiomatic HoTT" (Martin-Löf intensional type theory with univalence and higher inductive types added by axioms) by defining appropriate abstractions. These two lectures will explain how the syntax of cubical type theory differs from axiomatic HoTT, and how this simplifies constructions using higher inductive types. No prior knowledge of cubical models or methods will be presumed.