EXACT COMPLETION AND CONSTRUCTIVE THEORIES OF SETS

DOI10.1017/jsl.2020.2zbMath1485.03257arXiv1710.10685OpenAlexW2766895680MaRDI QIDQ5148098

Erik Palmgren, Jacopo Emmenegger

Publication date: 29 January 2021

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

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

zbMATH Keywords

constructive set theorycategorical logicexact completionsetoidslocal Cartesian closure

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Topoi (18B25) Categories admitting limits (complete categories), functors preserving limits, completions (18A35) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Intuitionistic mathematics (03F55) Categories of sets, characterizations (18B05) Foundations, relations to logic and deductive systems (18A15) Type theory (03B38)

Related Items

Flatness, weakly lex colimits, and free exact completions, W-types in setoids, The effective model structure and -groupoid objects

Uses Software

• GitHub

Cites Work

• Quotient completion for the foundation of constructive mathematics
• Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets
• Inductive types and exact completion
• Aspects of predicative algebraic set theory. I: Exact completion
• Regular and exact completions
• Wellfounded trees in categories
• Locally cartesian closed exact completions
• Weak subobjects and the epi-monic completion of a category.
• Exact completion of path categories and algebraic set theory. I: Exact completion of path categories
• Some free constructions in realizability and proof theory
• On the local Cartesian closure of exact completions
• Elementary quotient completion
• Constructing categories and setoids of setoids in type theory
• Colimit completions and the effective topos
• On the axiom of extensionality – Part I
• Setoids and universes
• Adjointness in Foundations
• A categorical version of the BrouwerHeytingKolmogorov interpretation
• Relating Quotient Completions via Categorical Logic
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item