Elementary quotient completion

Abstract

We extend the notion of exact completion on a weakly lex category to elementary doctrines. We show how any such doctrine admits an elementary quotient completion, which freely adds effective quotients and extensional equality. We note that the elementary quotient completion can be obtained as the composite of two free constructions: one adds effective quotients, and the other forces extensionality of maps. We also prove that each construction preserves comprehensions.

References in corpus (2)

• A minimalist two-level foundation for constructive mathematics
• Quotient completion for the foundation of constructive mathematics

Cited by in corpus (8)

• Sets in homotopy type theory
• Exact completion and constructive theories of sets
• Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice
• A co-free construction for elementary doctrines
• A realizability semantics for inductive formal topologies, Church's Thesis and Axiom of Choice
• Remarks on the Tripos To Topos Construction: extensionality, comprehensions, quotients and cauchy-complete objects
• A Fibrational Tale of Operational Logical Relations: Pure, Effectful and Differential
• Biased elementary doctrines and quotient completions