Elementary quotient completion
From MaRDI portal
Publication:2855642
zbMATH Open1288.03048arXiv1206.0162MaRDI QIDQ2855642FDOQ2855642
Authors: Maria Emilia Maietti, Giuseppe Rosolini 
Publication date: 25 October 2013
Published in: Theory and Applications of Categories (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1206.0162
File on IPFS (Hint: this is only the Hash - if you get a timeout, this file is not available on our server.)
Recommendations
Categorical logic, topoi (03G30) Categorical semantics of formal languages (18C50) Intuitionistic mathematics (03F55)
Cited In (40)
- On a generalization of equilogical spaces
- Unifying exact completions
- A characterisation of elementary fibrations
- The existential completion
- Remarks on the tripos to topos construction: comprehension, extensionality, quotients and functional-completeness
- A fibrational tale of operational logical relations: pure, effectful and differential
- Quotient completion for the foundation of constructive mathematics
- On choice rules in dependent type theory
- Title not available (Why is that?)
- Elementary fibrations of enriched groupoids
- A characterization of generalized existential completions
- Frames and topological algebras for a double-power monad
- Elementary doctrines as coalgebras
- Quotients, pure existential completions and arithmetic universes
- Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice
- Homotopies in Grothendieck fibrations
- From type theory to setoids and back
- Factorizing the \(\mathbf{Top}\)-\(\mathbf{Loc}\) adjunction through positive topologies
- Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator
- Quotients and extensionality in relational doctrines
- Relating quotient completions via categorical logic
- Flatness, weakly lex colimits, and free exact completions
- Adding a constant and an axiom to a doctrine
- A co-free construction for elementary doctrines
- Doctrines, modalities and comonads
- Logical foundations of quantitative equality
- Equilogical spaces and algebras for a double-power monad
- Title not available (Why is that?)
- Equiconsistency of the minimalist foundation with its classical version
- Left adjoint to precomposition in elementary doctrines
- Exact completion and constructive theories of sets
- Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice
- A categorical reading of the numerical existence property in constructive foundations
- Numerical existence property and categories with an internal copy
- Categories of partial equivalence relations as localizations
- A PREDICATIVE VARIANT OF HYLAND’S EFFECTIVE TOPOS
- The compatibility of the minimalist foundation with homotopy type theory
- A property of effectivization and its uses in categorical logic
- On linear exactness properties
- A characterization of those categories whose internal logic is Hilbert's \(\varepsilon\)-calculus
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)
