Evan Cavallo: Interpreting cubical types as spaces

Abstract

Cubical type theories, like univalent type theories more generally, are often used as tools for reasoning about "topological spaces". To formally justify this, we want a cubical type theory with a semantics where types are interpreted as representations of spaces, a criterion we can make precise using tools from homotopy theory. I'll outline the current state of the art: which interpretations are known to present spaces, which are known not to, and which remain in limbo. In particular, I'll describe a semantics presenting spaces where types are interpreted as so-called equivariant fibrations in cartesian cubical sets; this semantics is developed in joint work with Steve Awodey, Thierry Coquand, Emily Riehl, and Christian Sattler. Time permitting, I'll conclude with some speculation on future directions.