Relative elegance and cartesian cubes with one connection

TL;DR

This paper demonstrates a Quillen equivalence between two models of homotopy type theory using cartesian cubical sets with one connection, advancing the understanding of constructive models of infinity-groupoids.

Contribution

It establishes a new model structure on cartesian cubical sets with one connection that models homotopy type theory and presents infinity-groupoids, complementing existing models.

Findings

Proves a Quillen equivalence between two model structures.

Identifies a new constructive model of homotopy type theory.

Provides a model that presents infinity-groupoids.

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.