5 found
Sort by:
  1. Steve Awodey & Michael A. Warren, Homotopy Theoretic Models of Identity Types.
    Quillen [17] 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 [15] or the work of Joyal [11, 12] and Lurie [13] 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 (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  2. Pieter Hofstra & Michael A. Warren (2013). Combinatorial Realizability Models of Type Theory. Annals of Pure and Applied Logic 164 (10):957-988.
    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 (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  3. Michael A. Warren (2007). Coalgebras in a Category of Classes. Annals of Pure and Applied Logic 146 (1):60-71.
    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.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  4. Steve Awodey, Henrik Forssell & Michael A. Warren, Algebraic Models of Sets and Classes in Categories of Ideals.
    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 [17], 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.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  5. Steve Awodey & Michael A. Warren, Predicative Algebraic Set Theory.
    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 (...)
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation