Skip to main content
To KTH's start page

Evan Cavallo: Interpreting cubical types as spaces

Time: Thu 2024-10-03 15.00 - 16.00

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

Participating: Evan Cavallo (Gothenburg)

Export to calendar

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.