Elementary quotient completion

MaRDI QIDQ2855642zbMATH OpenFDO

Authors Maria Emilia Maietti, Giuseppe Rosolini

Publication date 25 October 2013

Published in Theory and Applications of Categories (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1206.0162, http://www.emis.de/journals/TAC/volumes/27/17/27-17abs.html

IPFS File on IPFS (Hint: this is only the Hash - if you get a timeout, this file is not available on our server.)

zbMATH Keywords

quotient completionsplit fibrationelementary doctrines

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Categorical semantics of formal languages (18C50) Intuitionistic mathematics (03F55)

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

• Relating quotient completions via categorical logic
• The existential completion
• Unifying exact completions
• Elementary doctrines as coalgebras
• Quotient completion for the foundation of constructive mathematics

Cited in

(40)

• On a generalization of equilogical spaces
• A characterisation of elementary fibrations
• Remarks on the tripos to topos construction: comprehension, extensionality, quotients and functional-completeness
• Unifying exact completions
• The existential completion
• Quotient completion for the foundation of constructive mathematics
• A fibrational tale of operational logical relations: pure, effectful and differential
• On choice rules in dependent type theory
• scientific article; zbMATH DE number 7080197 (Why is no real title available?)
• 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
• A co-free construction for elementary doctrines
• Adding a constant and an axiom to a doctrine
• Doctrines, modalities and comonads
• Equilogical spaces and algebras for a double-power monad
• Logical foundations of quantitative equality
• scientific article; zbMATH DE number 7379292 (Why is no real title available?)
• Exact completion and constructive theories of sets
• Equiconsistency of the minimalist foundation with its classical version
• Left adjoint to precomposition in elementary doctrines
• 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
• A characterization of those categories whose internal logic is Hilbert's \(\varepsilon\)-calculus
• On linear exactness properties

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)