Lawvere–Tierney sheaves in Algebraic Set Theory

DOI10.2178/JSL/1245158088MaRDI QIDQ3399181zbMATH OpenOpenAlexWikidataFDO

Authors Nicola Gambino, Peter Lefanu Lumsdaine, Michael A. Warren, Steve Awodey

Publication date 29 September 2009

Published in Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/0711.1529

zbMATH Keywords

algebraic set theoryLawvere-Tierney coveragesLawvere-Tierney sheaves

Mathematics Subject Classification ID

Categories of sets, characterizations (18B05) Nonclassical and second-order set theories (03E70) Categorical logic, topoi (03G30) Topoi (18B25)

Abstract: 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.

Recommendations

• scientific article; zbMATH DE number 4095456
• Aspects of predicative algebraic set theory. III: Sheaves
• The associated sheaf functor theorem in algebraic set theory
• Lawvere-Tierney sheafification in Homotopy Type Theory
• scientific article; zbMATH DE number 4181608

Cites work

• scientific article; zbMATH DE number 1840601 (Why is no real title available?)
• Aspects of predicative algebraic set theory. I: Exact completion
• Coalgebras in a category of classes
• Heyting-valued interpretations for constructive set theory
• Independence results around constructive ZF
• Regular and exact completions
• Sheaf models for set theory
• Some free constructions in realizability and proof theory
• The associated sheaf functor theorem in algebraic set theory
• The axiom of choice
• Type theories, toposes and constructive set theory: Predicative aspects of AST

Cited in

(7)

• scientific article; zbMATH DE number 4095456 (Why is no real title available?)
• The associated sheaf functor theorem in algebraic set theory
• Lawvere-Tierney sheafification in Homotopy Type Theory
• Higher order functions and Brouwer's thesis
• Lawvere-Tierney sheaves, factorization systems, sections and \(j\)-essential monomorphisms in a topos
• Aspects of predicative algebraic set theory. III: Sheaves
• Relativized Grothendieck topoi

This page was built for publication: Lawvere–Tierney sheaves in Algebraic Set Theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3399181)