Quillen  introduced model categories as an abstract framework for homotopy theory which would apply to a wide range of mathematical settings. By all accounts this program has been a success and—as, e.g., the work of Voevodsky on the homotopy theory of schemes  or the work of Joyal [11, 12] and Lurie  on quasicategories seem to indicate—it will likely continue to facilitate mathematical advances. In this paper we present a novel connection between model categories and mathematical logic, inspired (...) by the groupoid model of (intensional) Martin–Löf type theory  due to Hofmann and Streicher . In particular, we show that a form of Martin–Löf type theory can be soundly modelled in any model category. This result indicates moreover that any model category has an associated “internal language” which is itself a form of Martin-Löf type theory. This suggests applications both to type theory and to homotopy theory. Because Martin–Löf type theory is, in one form or another, the theoretical basis for many of the computer proof assistants currently in use, such as Coq and Agda (cf.  and ), this promise of applications is of a practical, as well as theoretical, nature. This paper provides a precise indication of this connection between homotopy theory and logic; a more detailed discussion of these and further results will be given in . (shrink)
In this paper the machinery and results developed in [Awodey et al, 2004] are extended to the study of constructive set theories. Specifically, we introduce two constructive set theories BCST and CST and prove that they are sound and complete with respect to models in categories with certain structure. Specifically, basic categories of classes and categories of classes are axiomatized and shown to provide models of the aforementioned set theories. Finally, models of these theories are constructed in the category of (...) ideals. (shrink)
In this short note we give a glimpse of homotopy type theory, a new field of mathematics at the intersection of algebraic topology and mathematical logic, and we explain Vladimir Voevodsky’s univalent interpretation of it. This interpretation has given rise to the univalent foundations program, which is the topic of the current special year at the Institute for Advanced Study.
We introduce a new model construction for Martin-Löf intensional type theory, which is sound and complete for the 1-truncated version of the theory. The model formally combines, by gluing along the functor from the category of contexts to the category of groupoids, the syntactic model with a notion of realizability. As our main application, we use the model to analyse the syntactic groupoid associated to the type theory generated by a graph G, showing that it has the same homotopy type (...) as the free groupoid generated by G. (shrink)
In this paper the familiar construction of the category of coalgebras for a cartesian comonad is extended to the setting of “algebraic set theory”. In particular, it is shown that, under suitable assumptions, several kinds of categories of classes are stable under the formation of coalgebras for a cartesian comonad, internal presheaves and comma categories.
We introduce a new sheaf-theoretic construction called the ideal completion of a category and investigate its logical properties. We show that it satisfies the axioms for a category of classes in the sense of Joyal and Moerdijk , so that the tools of algebraic set theory can be applied to produce models of various elementary set theories. These results are then used to prove the conservativity of different set theories over various classical and constructive type theories.