Evan Cavallo: Unifying cubical type theories

Abstract

The push to find a computational interpretation for homotopy type theory led to the development first of multiple models of HoTT based on cubical sets, then corresponding cubical type theories which can serve as computational alternatives to HoTT. The various type theories and models appear similar, but are not self-evidently instances of some single family of theories or model construction. I will present joint work with Anders Mörtberg and Andrew Swan from 2020 which unifies the so-called "structural" cubical theories and models, giving a parameterized definition which can be applied with different choices of interval structure and cofibrations. I will also discuss the still-open problems in this area, such as the case of substructural cubical models.