works on
categories 1homotopy type theory 1induction principles 1simplicial type theory 1spaces 1univalence 1

From the 1 of 3 linked papers with an AI index.

collaborators
Showing math.ATShow all

1 paper · 1 filter

math.AT2026

The equivariant model structure on cartesian cubical sets

Steve Awodey, Evan Cavallo, Thierry Coquand +2

We develop a constructive model of homotopy type theory in a Quillen model category that classically presents the usual homotopy theory of spaces. Our model is based on presheaves…