Model structure on the universe of all types in interval type theory

International audienceModel categories constitute the major context for doing homotopy theory. More recently, Homotopy Type Theory has been introduced as a context for doing syntactic homotopy theory. In this paper, we show that a slight generalization of Homotopy Type Theory, called Interval Type Theory, allows to define a model structure on the universe of all types, which, through the model interpretation, corresponds to defining a model structure on the category of cubical sets. This work generalizes previous works of Gambino, Garner and Lumsdaine from the universe of fibrant types to the universe of all types. Our definition of Interval Type Theory comes from the work of Orton and Pitts to define a syntactic approximation of the internal language of the category of cubical sets. In this paper, we extend the work of Orton and Pitts by introducing the notion of degenerate fibrancy, which allows to define a fibrant replacement, at the heart of the model structure on the universe of all types. All our definitions and propositions have been formalized using the Coq proof assistant