We give an overview of recent work on proper cofibrantly generated algebraic model structures in certain variants of cubical sets, with attention paid to issues of constructivity.

This is in connection with Coquand et al.'s work on the cubical model of type theory and also earlier work by Cisinski.