Elementary quotient completion
From MaRDI portal
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.
Recommendations
Cited in
(45)- On a generalization of equilogical spaces
- Equilogical spaces and algebras for a double-power monad
- Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator
- A characterization of those categories whose internal logic is Hilbert's \(\varepsilon\)-calculus
- Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice
- On linear exactness properties
- A categorical reading of the numerical existence property in constructive foundations
- A characterisation of elementary fibrations
- Numerical existence property and categories with an internal copy
- Elementary doctrines as coalgebras
- Factorizing the \(\mathbf{Top}\)-\(\mathbf{Loc}\) adjunction through positive topologies
- A co-free construction for elementary doctrines
- Unifying exact completions
- Remarks on the tripos to topos construction: comprehension, extensionality, quotients and functional-completeness
- A characterization of generalized existential completions
- Categories of partial equivalence relations as localizations
- On choice rules in dependent type theory
- Homotopies in Grothendieck fibrations
- Quotient completion for the foundation of constructive mathematics
- scientific article; zbMATH DE number 7080197 (Why is no real title available?)
- A property of effectivization and its uses in categorical logic
- A realizability semantics for inductive formal topologies, Church's thesis and axiom of choice
- Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice
- Doctrines, modalities and comonads
- Elementary fibrations of enriched groupoids
- The existential completion
- Exact completion and constructive theories of sets
- A PREDICATIVE VARIANT OF HYLAND’S EFFECTIVE TOPOS
- Frames and topological algebras for a double-power monad
- Relating quotient completions via categorical logic
- From type theory to setoids and back
- The compatibility of the minimalist foundation with homotopy type theory
- Flatness, weakly lex colimits, and free exact completions
- Left adjoint to precomposition in elementary doctrines
- A fibrational tale of operational logical relations: pure, effectful and differential
- Quotients, pure existential completions and arithmetic universes
- Quotients and extensionality in relational doctrines
- Adding a constant and an axiom to a doctrine
- Logical foundations of quantitative equality
- Equiconsistency of the minimalist foundation with its classical version
- The relational quotient completion
- Quantifier-free formulas and quantifier alternation depth in doctrines
- Biased elementary doctrines and quotient completions
- Quantitative equality in substructural logic via Lipschitz doctrines
- When Lawvere meets Peirce: an equational presentation of Boolean hyperdoctrines
This page was built for publication: Elementary quotient completion
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2855642)
