1.  22
    Heyting-Valued Interpretations for Constructive Set Theory.Nicola Gambino - 2006 - Annals of Pure and Applied Logic 137 (1):164-188.
    We define and investigate Heyting-valued interpretations for Constructive Zermelo–Frankel set theory . These interpretations provide models for CZF that are analogous to Boolean-valued models for ZF and to Heyting-valued models for IZF. Heyting-valued interpretations are defined here using set-generated frames and formal topologies. As applications of Heyting-valued interpretations, we present a relative consistency result and an independence proof.
    Direct download (5 more)  
    Export citation  
    Bookmark   16 citations  
  2.  33
    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 (5 more)  
    Export citation  
    Bookmark   7 citations  
  3.  9
    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