Unifying exact completions
From MaRDI portal
Publication:2254599
Abstract: We define the notion of exact completion with respect to an existential elementary doctrine. We observe that the forgetful functor from the 2-category exact categories to existential elementary doctrines has a left biadjoint that can be obtained as a composite of two others. Finally, we conclude how this notion encompasses both that of the exact completion of a regular category as well as that of the exact completion of a cartesian category with weak pullbacks.
Recommendations
Cites work
- A co-free construction for elementary doctrines
- A minimalist two-level foundation for constructive mathematics
- Adjointness in Foundations
- Cartesian bicategories. I
- Categorical logic and type theory
- Elementary quotient completion
- Exact categories and categories of sheaves
- Factorization systems and fibrations: toward a fibred Birkhoff variety theorem
- scientific article; zbMATH DE number 3851091 (Why is no real title available?)
- scientific article; zbMATH DE number 5695342 (Why is no real title available?)
- scientific article; zbMATH DE number 4061468 (Why is no real title available?)
- scientific article; zbMATH DE number 19493 (Why is no real title available?)
- scientific article; zbMATH DE number 45228 (Why is no real title available?)
- scientific article; zbMATH DE number 50149 (Why is no real title available?)
- scientific article; zbMATH DE number 3554463 (Why is no real title available?)
- scientific article; zbMATH DE number 3794304 (Why is no real title available?)
- scientific article; zbMATH DE number 1913781 (Why is no real title available?)
- scientific article; zbMATH DE number 3346618 (Why is no real title available?)
- scientific article; zbMATH DE number 3370546 (Why is no real title available?)
- Quotient completion for the foundation of constructive mathematics
- Realizability. An introduction to its categorical side
- Regular and exact completions
- Setoids in type theory
- Some free constructions in realizability and proof theory
- Tripos theory
- Tripos theory in retrospect
Cited in
(40)- Cartesian closed exact completions
- Smyth completion as bicompletion
- 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
- A unified functional look at completion in MET, UNIF and AP
- On linear exactness properties
- Dialectica logical principles
- Elementary doctrines as coalgebras
- Dialectica principles via Gödel doctrines
- A characterization of generalized existential completions
- Uniform ideal completions
- Elementary quotient completion
- Exact completions and small sheaves
- On choice rules in dependent type theory
- Detecting completeness from Ext-vanishing
- 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
- Relating quotient completions via categorical logic
- A topos for continuous logic
- On categorical structures arising from implicative algebras: from topology to assemblies
- Quotients, pure existential completions and arithmetic universes
- Logical foundations of quantitative equality
- Equiconsistency of the minimalist foundation with its classical version
- Quantifier-free formulas and quantifier alternation depth in doctrines
- Biased elementary doctrines and quotient completions
- Categorifying computable reducibilities
- Quantitative equality in substructural logic via Lipschitz doctrines
- When Lawvere meets Peirce: an equational presentation of Boolean hyperdoctrines
- Effectiveness and continuity in intuitionistic quasi-toposes of assemblies
- Existential completions and Herbrand's theorem
- A topos for extended Weihrauch degrees
- On Boolean hyperdoctrines and peircean bicategories
- A theorem on Barr-exact categories, with an infinitary generalization
This page was built for publication: Unifying exact completions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2254599)
