Switch to: References

Add citations

You must login to add citations.
  1. Lawvere-Tierney Sheaves in Algebraic Set Theory.S. Awodey, N. Gambino & M. A. Warren - 2009 - Journal of Symbolic Logic 74 (3):861 - 890.
    We present a solution to the problem of defining a counterpart in Algebraic Set Theory of the construction of internal sheaves in Topos Theory. Our approach is general in that we consider sheaves as determined by Lawvere-Tierney coverages, rather than by Grothendieck coverages, and assume only a weakening of the axioms for small maps originally introduced by Joyal and Moerdijk, thus subsuming the existing topos-theoretic results.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • Regular Universes and Formal Spaces.Erik Palmgren - 2006 - Annals of Pure and Applied Logic 137 (1):299-316.
    We present an alternative solution to the problem of inductive generation of covers in formal topology by using a restricted form of type universes. These universes are at the same time constructive analogues of regular cardinals and sets of infinitary formulae. The technique of regular universes is also used to construct canonical positivity predicates for inductively generated covers.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  • The Associated Sheaf Functor Theorem in Algebraic Set Theory.Nicola Gambino - 2008 - Annals of Pure and Applied Logic 156 (1):68-77.
    We prove a version of the associated sheaf functor theorem in Algebraic Set Theory. The proof is established working within a Heyting pretopos equipped with a system of small maps satisfying the axioms originally introduced by Joyal and Moerdijk. This result improves on the existing developments by avoiding the assumption of additional axioms for small maps and the use of collection sites.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • Topological Inductive Definitions.Giovanni Curi - 2012 - Annals of Pure and Applied Logic 163 (11):1471-1483.
    In intuitionistic generalized predicative systems as constructive set theory, or constructive type theory, two categories have been proposed to play the role of the category of locales: the category FSp of formal spaces, and its full subcategory FSpi of inductively generated formal spaces. Considered in impredicative systems as the intuitionistic set theory IZF, FSp and FSpi are both equivalent to the category of locales. However, in the mentioned predicative systems, FSp fails to be closed under basic constructions such as that (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • Generalizing Realizability and Heyting Models for Constructive Set Theory.Albert Ziegler - 2012 - Annals of Pure and Applied Logic 163 (2):175-184.
  • Aspects of Predicative Algebraic Set Theory I: Exact Completion.Benno van den Berg & Ieke Moerdijk - 2008 - Annals of Pure and Applied Logic 156 (1):123-159.
    This is the first in a series of papers on Predicative Algebraic Set Theory, where we lay the necessary groundwork for the subsequent parts, one on realizability [B. van den Berg, I. Moerdijk, Aspects of predicative algebraic set theory II: Realizability, Theoret. Comput. Sci. . Available from: arXiv:0801.2305, 2008], and the other on sheaves [B. van den Berg, I. Moerdijk, Aspects of predicative algebraic set theory III: Sheaf models, 2008 ]. We introduce the notion of a predicative category with small (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  • Derived Rules for Predicative Set Theory: An Application of Sheaves.Benno van den Berg & Ieke Moerdijk - 2012 - Annals of Pure and Applied Logic 163 (10):1367-1383.
  • Abstract Inductive and Co-Inductive Definitions.Giovanni Curi - 2018 - Journal of Symbolic Logic 83 (2):598-616.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  • Sublocales in Formal Topology.Steven Vickers - 2007 - Journal of Symbolic Logic 72 (2):463 - 482.
    The paper studies how the localic notion of sublocale transfers to formal topology. For any formal topology (not necessarily with positivity predicate) we define a sublocale to be a cover relation that includes that of the formal topology. The family of sublocales has set-indexed joins. For each set of base elements there are corresponding open and closed sublocales, boolean complements of each other. They generate a boolean algebra amongst the sublocales. In the case of an inductively generated formal topology, the (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  • The Relation Reflection Scheme.Peter Aczel - 2008 - Mathematical Logic Quarterly 54 (1):5-11.
    We introduce a new axiom scheme for constructive set theory, the Relation Reflection Scheme . Each instance of this scheme is a theorem of the classical set theory ZF. In the constructive set theory CZF–, when the axiom scheme is combined with the axiom of Dependent Choices , the result is equivalent to the scheme of Relative Dependent Choices . In contrast to RDC, the scheme RRS is preserved in Heyting-valued models of CZF– using set-generated frames. We give an application (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  • The Generalised Type-Theoretic Interpretation of Constructive Set Theory.Nicola Gambino & Peter Aczel - 2006 - Journal of Symbolic Logic 71 (1):67 - 103.
    We present a generalisation of the type-theoretic interpretation of constructive set theory into Martin-Löf type theory. The original interpretation treated logic in Martin-Löf type theory via the propositions-as-types interpretation. The generalisation involves replacing Martin-Löf type theory with a new type theory in which logic is treated as primitive. The primitive treatment of logic in type theories allows us to study reinterpretations of logic, such as the double-negation translation.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  • On Some Peculiar Aspects of the Constructive Theory of Point-Free Spaces.Giovanni Curi - 2010 - Mathematical Logic Quarterly 56 (4):375-387.
    This paper presents several independence results concerning the topos-valid and the intuitionistic predicative theory of locales. In particular, certain consequences of the consistency of a general form of Troelstra's uniformity principle with constructive set theory and type theory are examined.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  • A Cumulative Hierarchy of Sets for Constructive Set Theory.Albert Ziegler - 2014 - Mathematical Logic Quarterly 60 (1-2):21-30.
  • Kripke Models for Subtheories of CZF.Rosalie Iemhoff - 2010 - Archive for Mathematical Logic 49 (2):147-167.
    In this paper a method to construct Kripke models for subtheories of constructive set theory is introduced that uses constructions from classical model theory such as constructible sets and generic extensions. Under the main construction all axioms except the collection axioms can be shown to hold in the constructed Kripke model. It is shown that by carefully choosing the classical models various instances of the collection axioms, such as exponentiation, can be forced to hold as well. The paper does not (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation