Derived rules for predicative set theory: an application of sheaves

DOI10.1016/j.apal.2012.01.010zbMath1432.03128arXiv1009.3553OpenAlexW2143931279MaRDI QIDQ448333

Benno van den Berg, Ieke Moerdijk

Publication date: 6 September 2012

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

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

zbMATH Keywords

Baire spacesheavesconstructive set theoryderived rules

Mathematics Subject Classification ID

Nonclassical and second-order set theories (03E70) Metamathematics of constructive systems (03F50) Presheaves and sheaves, stacks, descent conditions (category-theoretic aspects) (18F20)

Related Items (4)

Non-deterministic inductive definitions ⋮ Formally continuous functions on Baire space ⋮ THE FIRST-ORDER LOGIC OF CZF IS INTUITIONISTIC FIRST-ORDER LOGIC ⋮ The axiom of multiple choice and models for constructive set theory

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Aspects of predicative algebraic set theory. II: Realizability
• Inductive types and exact completion
• Aspects of predicative algebraic set theory. I: Exact completion
• Constructivism in mathematics. An introduction. Volume I
• Sheaves in geometry and logic: a first introduction to topos theory
• Inductively generated formal topologies.
• Some points in formal topology.
• Wellfounded trees in categories
• Aspects of general topology in constructive set theory
• Heyting-valued interpretations for constructive set theory
• The axiom of multiple choice and models for constructive set theory
• Heine-Borel does not imply the Fan Theorem
• Forcing in intuitionistic systems without power-set
• Derived rules related to a constructive theory of metric spaces in intuitionistic higher order arithmetic without countable choice
• Principles of continuous choice and continuity of functions in formal systems for constructive mathematics
• A note on Bar Induction in Constructive Set Theory
• The disjunction and related properties for constructive Zermelo-Fraenkel set theory
• W-types in homotopy type theory
• Type theories, toposes and constructive set theory: Predicative aspects of AST

This page was built for publication: Derived rules for predicative set theory: an application of sheaves