Lawvere–Tierney sheaves in Algebraic Set Theory

DOI10.2178/JSL/1245158088zbMATH Open1183.03068arXiv0711.1529OpenAlexW3100082872WikidataQ61834699 ScholiaQ61834699MaRDI QIDQ3399181FDOQ3399181

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)

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.

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

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

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)

Cites Work

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

Cited In (7)

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

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)