Abstract: Tim Campion, Chris Kapulkin and I recently proposed certain (marked) cubical sets as a model for weak $\omega$-categories (a.k.a. $(\infty,\infty)$-categories). This model is a sort of cubical adaptation of Verity's complicial sets (which are simplicial), and we made the analogy more precise (than a mere resemblance of definitions) by proving the triangulation functor to be left Quillen and strong monoidal with respect to both lax and pseudo Gray tensor products. In this talk, I will define these models, explain the intuition behind the definitions, and give a flavour of the sort of combinatorics that went into the proofs.