A convenient category of cubes
Sanjeevi Krishnan, Emily Rudman
TL;DR
This paper introduces the cube category $\boxplus$, whose objects are finite Boolean lattices and whose morphisms are interval-preserving monotone maps, as a convenient general-purpose site for cubical sets. It proves that $\boxplus$ is the largest concrete Eilenberg–Zilber variant excluding reversals and diagonals and provides a monoidal generator description, a Dold–Kan-type correspondence, and a Quillen-equivalent model structure to simplicial sets via triangulation, with properness ensuring interpretation of Martin–Löf dependent types. The work further develops Boolean complexes, subdivision, and nonpositive curvature via CAT(0) geometry, and analyzes the relationships between cubical and simplicial homotopy theories, including left-inducing model structures and triangulation compatibilities. These results offer a robust, constructive foundation for cubical homotopy theory, directed topology, and higher-order datatype modeling, with practical implications for computer-assisted proofs and type-theoretic interpretations.
Abstract
We claim that the cube category whose morphisms are the interval-preserving monotone functions between finite Boolean lattices is a convenient general-purpose site for cubical sets. This category is the largest possible concrete Eilenberg-Zilber variant excluding the reversals and diagonals. The category admits as monoidal generators all functions between the singleton and two-element ordinals and all monotone surjections from finite Boolean lattices to the two-element ordinal. Consequently, morphisms in the minimal symmetric monoidal variant of the cube category containing coconnections of one kind can be characterized as the interval-preserving semilattice homomorphisms between finite Boolean lattices. There exists a model structure on our variant of cubical sets that is at once Quillen equivalent to and left induced from the classical model structure on simplicial sets along triangulation. This model structure is proper and hence its fibrations interpret Martin-Lof dependent types.