Cartesian Cubical Model Categories

This book introduces the category of Cartesian cubical sets and endows it with a Quillen model structure using ideas coming from Homotopy type theory. In particular, recent constructions of cubical systems of univalent type theory are used to determine abstract homotopical semantics of type theory. The celebrated univalence axiom of Voevodsky plays a key role in establishing the basic laws of a mo...