Quotient completion for the foundation of constructive mathematics
From MaRDI portal
Abstract: We apply some tools developed in categorical logic to give an abstract description of constructions used to formalize constructive mathematics in foundations based on intensional type theory. The key concept we employ is that of a Lawvere hyperdoctrine for which we describe a notion of quotient completion. That notion includes the exact completion on a category with weak finite limits as an instance as well as examples from type theory that fall apart from this.
Recommendations
Cites work
- A minimalist two-level foundation for constructive mathematics
- Adjointness in Foundations
- Categorical logic and type theory
- Factorization systems and fibrations: toward a fibred Birkhoff variety theorem
- First order categorical logic. Model-theoretical methods in the theory of topoi and related categories
- scientific article; zbMATH DE number 3959364 (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 1289305 (Why is no real title available?)
- scientific article; zbMATH DE number 1302065 (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 877751 (Why is no real title available?)
- scientific article; zbMATH DE number 1392302 (Why is no real title available?)
- scientific article; zbMATH DE number 3291139 (Why is no real title available?)
- scientific article; zbMATH DE number 3370546 (Why is no real title available?)
- scientific article; zbMATH DE number 2247253 (Why is no real title available?)
- Locally cartesian closed exact completions
- Modular correspondence between dependent type theories and categories including pretopoi and topoi
- Realizability. An introduction to its categorical side
- Regular and exact completions
- Setoids in type theory
- Some free constructions in realizability and proof theory
Cited in
(53)- The essence of ideal completion in quantitative form
- On a generalization of equilogical spaces
- Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator
- Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice
- A characterisation of elementary fibrations
- Dialectica logical principles
- On the local Cartesian closure of exact completions
- Elementary doctrines as coalgebras
- Factorizing the \(\mathbf{Top}\)-\(\mathbf{Loc}\) adjunction through positive topologies
- A co-free construction for elementary doctrines
- Unifying exact completions
- Quotient topologies in constructive set theory and type theory
- Remarks on the tripos to topos construction: comprehension, extensionality, quotients and functional-completeness
- Dialectica principles via Gödel doctrines
- A characterization of generalized existential completions
- Elementary quotient completion
- On choice rules in dependent type theory
- An induction principle for consequence in arithmetic universes
- Triposes, q-toposes and toposes
- scientific article; zbMATH DE number 7080197 (Why is no real title available?)
- 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
- Constructions of categories of setoids from proof-irrelevant families
- The existential completion
- Exact completion and constructive theories of sets
- W-types in setoids
- A PREDICATIVE VARIANT OF HYLAND’S EFFECTIVE TOPOS
- From type theory to setoids and back
- The compatibility of the minimalist foundation with homotopy type theory
- Left adjoint to precomposition in elementary doctrines
- A presheaf semantics for quantified temporal logics
- 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
- Categorical models of subtyping
- The Kock-Mikkelsen factorisation
- Relating homotopy equivalences to conservativity in dependent type theories with computation axioms
- Cauchy completions and the rule of unique choice in relational doctrines
- Quantifier-free formulas and quantifier alternation depth in doctrines
- Diagrammatic algebra of first order logic
- 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
- A topos for extended Weihrauch degrees
- The calculus of neo-Peircean relations
- On Boolean hyperdoctrines and peircean bicategories
This page was built for publication: Quotient completion for the foundation of constructive mathematics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q382422)
