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
- 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?)
- 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
- 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
(38)- On a generalization of equilogical spaces
- Quotient topologies in constructive set theory and type theory
- A characterisation of elementary fibrations
- Remarks on the tripos to topos construction: comprehension, extensionality, quotients and functional-completeness
- Unifying exact completions
- The existential completion
- A presheaf semantics for quantified temporal logics
- 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
- An induction principle for consequence in arithmetic universes
- The essence of ideal completion in quantitative form
- 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
- From type theory to setoids and back
- Dialectica principles via Gödel doctrines
- Factorizing the \(\mathbf{Top}\)-\(\mathbf{Loc}\) adjunction through positive topologies
- Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator
- Dialectica logical principles
- On the local Cartesian closure of exact completions
- Quotients and extensionality in relational doctrines
- W-types in setoids
- Triposes, q-toposes and toposes
- A co-free construction for elementary doctrines
- Adding a constant and an axiom to a doctrine
- Elementary quotient completion
- Doctrines, modalities and comonads
- 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
- Constructions of categories of setoids from proof-irrelevant families
- A PREDICATIVE VARIANT OF HYLAND’S EFFECTIVE TOPOS
- The compatibility of the minimalist foundation with homotopy type theory
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)
