Relative elegance and cartesian cubes with one connection

Evan Cavallo, Christian Sattler

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…