Relative elegance and cartesian cubes with one connection
Evan Cavallo, Christian Sattler
TL;DR
The work constructs a robust constructive model for homotopy type theory by placing a cubical-type model on cartesian cubical sets with one connection and proving a Quillen equivalence to the classical Kan–Quillen model on simplicial sets, thereby presenting an $\infty$-groupoid-presenting, constructive interpretation of HoTT. The core technical innovations include (i) developing a disjunctive-cubical, one-connection cube category $\square_{\lor}$, (ii) establishing a cubical-type model structure via a fibration-extension framework and universes, (iii) leveraging relative elegance to relate the non-Reedy cube setting to the simplicial world, and (iv) showing that the resulting model is Quillen-equivalent to the Kan–Quillen model and coincides with Cisinski’s test model structure. The results extend cubical approaches to a constructive-categorical setting and provide a concrete bridge between cubical and simplicial perspectives on $\infty$-groupoids, with implications for constructive HoTT interpretations and universe constructions. Overall, the paper advances a viable, category-theoretically rigorous path to obtaining constructive models of HoTT that faithfully present $\infty$-groupoids while handling non-Reedy cube categories via relative elegance and idempotent completion.
Abstract
We establish a Quillen equivalence between the Kan-Quillen model structure and a model structure, derived from a cubical model of homotopy type theory, on the category of cartesian cubical sets with one connection. We thereby identify a second model structure which both constructively models homotopy type theory and presents infinity-groupoids, the first example being the equivariant cartesian model of Awodey-Cavallo-Coquand-Riehl-Sattler.