Relative elegance and cartesian cubes with one connection
Algebraic Topology
2025-10-16 v6 Category Theory
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.
Cite
@article{arxiv.2211.14801,
title = {Relative elegance and cartesian cubes with one connection},
author = {Evan Cavallo and Christian Sattler},
journal= {arXiv preprint arXiv:2211.14801},
year = {2025}
}
Comments
61 pages. v6: Version accepted to Canadian Journal of Mathematics, modulo copy-editing