Cubical methods in homotopy type theory and univalent foundations

Cubical methods have played an important role in the development of Homotopy Type Theory and Univalent Foundations (HoTT/UF) in recent years. The original motivation behind these developments was to give constructive meaning to Voevodsky’s univalence axiom, but they have since then led to a range of new results. Among the achievements of these methods is the design of new type theories and proof assistants with native support for notions from HoTT/UF, syntactic and semantic consistency results for HoTT/UF, as well as a variety of independence results and establishing that the univalence axiom does not increase the proof theoretic strength of type theory. This paper is based on lecture notes that were written for the 2019 Homotopy Type Theory Summer School at Carnegie Mellon University. The goal of these lectures was to give an introduction to cubical methods and provide sufficient background in order to make the current research in this very active area of HoTT/UF more accessible to newcomers. The focus of these notes is hence on both the syntactic and semantic aspects of these methods, in particular on cubical type theory and the various cubical set categories that give meaning to these theories.

The twisted Cartesian model for the double path fibration

In this paper, the notion of a truncating twisting function from a cubical set to a permutahedral set and the corresponding notion of a twisted Cartesian product of these sets are introduced. The latter becomes a permutocubical set that models, in particular, the path fibration on a loop space. The chain complex of this twisted Cartesian product is in fact a comultiplicative twisted tensor product of cubical chains of base and permutahedral chains of fibre. This construction is formalized as a theory of twisted tensor products for Hirsch algebras.