Syntax and Models of Cartesian Cubical Type Theory

We present a cubical type theory based on the Cartesian cube category (faces, degeneracies, symmetries, diagonals, but no connections or reversal) with univalent universes, each containing Π, Σ, path, identity, natural number, boolean, pushout, and glue (equivalence extension) types. The type theory includes a syntactic description of a uniform Kan operation, along with judgemental equality rules defining the Kan operation on each type. The Kan operation uses both a different set of generating trivial cofibrations and a different set of generating cofibrations than the Cohen, Coquand, Huber, and Mörtberg (CCHM) model. Next, we describe a constructive model of this type theory in Cartesian cubical sets. We give a mechanized proof, using the internal language of cubical sets in the style introduced by Orton and Pitts, that glue, Π, Σ, path, identity, boolean, natural number, pushout types and the universe itself are Kan in this model, and that the universe is univalent. An advantage of this formal approach is that our construction can also be interpreted in cubical sets on the connections cube category, and on the de Morgan cube category used in the CCHM model. As a first step towards comparing these approaches, we show that the two Kan operations are interderivable in a setting where both exist (presheaves on the de Morgan cube category, with the additional cofibration required by our construction).