Model structure on the universe of all types in interval type theory - Ecole Centrale de Nantes Accéder directement au contenu
Article Dans Une Revue Mathematical Structures in Computer Science Année : 2020

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

Résumé

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.
Fichier principal
Vignette du fichier
model_structure_on_the_universe_of_all_types_in_interval_type_theory.pdf (1.53 Mo) Télécharger le fichier
Origine : Publication financée par une institution
Loading...

Dates et versions

hal-02966633 , version 1 (14-10-2020)

Identifiants

Citer

Simon Boulier, Nicolas Tabareau. Model structure on the universe of all types in interval type theory. Mathematical Structures in Computer Science, 2020, pp.1-32. ⟨10.1017/S0960129520000213⟩. ⟨hal-02966633⟩
158 Consultations
229 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More