Skip to Main content Skip to Navigation
Journal articles

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

Abstract : Model 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.
Document type :
Journal articles
Complete list of metadatas

Cited literature [29 references]  Display  Hide  Download

https://hal.inria.fr/hal-02966633
Contributor : Nicolas Tabareau <>
Submitted on : Wednesday, October 14, 2020 - 11:52:34 AM
Last modification on : Friday, October 16, 2020 - 3:12:14 AM

File

model_structure_on_the_univers...
Files produced by the author(s)

Identifiers

Citation

Simon Boulier, Nicolas Tabareau. Model structure on the universe of all types in interval type theory. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2020, pp.1-32. ⟨10.1017/S0960129520000213⟩. ⟨hal-02966633⟩

Share

Metrics

Record views

37

Files downloads

25