# Evan Cavallo: Interpreting cubical types as spaces

**Tid: **
To 2024-10-03 kl 15.00 - 16.00

**Plats: **
Albano house 1, floor 3, room 11 (Kovalevsky)

**Medverkande: **
Evan Cavallo (Gothenburg)

### 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.