Quotient completion for the foundation of constructive mathematics
From MaRDI portal
Publication:382422
DOI10.1007/s11787-013-0080-2zbMath1288.03049arXiv1202.1012OpenAlexW2065468423MaRDI QIDQ382422
Maria Emilia Maietti, Giuseppe Rosolini
Publication date: 19 November 2013
Published in: Logica Universalis (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1202.1012
Categorical logic, topoi (03G30) Categorical semantics of formal languages (18C50) Intuitionistic mathematics (03F55)
Related Items (27)
Remarks on the tripos to topos construction: comprehension, extensionality, quotients and functional-completeness ⋮ From type theory to setoids and back ⋮ A characterisation of elementary fibrations ⋮ Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice ⋮ Dialectica logical principles ⋮ Doctrines, modalities and comonads ⋮ On a generalization of equilogical spaces ⋮ Elementary fibrations of enriched groupoids ⋮ On the local Cartesian closure of exact completions ⋮ Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator ⋮ Dialectica principles via Gödel doctrines ⋮ The compatibility of the minimalist foundation with homotopy type theory ⋮ A characterization of generalized existential completions ⋮ Unnamed Item ⋮ An induction principle for consequence in arithmetic universes ⋮ Elementary doctrines as coalgebras ⋮ On Choice Rules in Dependent Type Theory ⋮ Triposes, q-toposes and toposes ⋮ EXACT COMPLETION AND CONSTRUCTIVE THEORIES OF SETS ⋮ Factorizing the \(\mathbf{Top}\)-\(\mathbf{Loc}\) adjunction through positive topologies ⋮ Constructions of categories of setoids from proof-irrelevant families ⋮ A PREDICATIVE VARIANT OF HYLAND’S EFFECTIVE TOPOS ⋮ Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice ⋮ A co-free construction for elementary doctrines ⋮ Unifying exact completions ⋮ The existential completion ⋮ W-types in setoids
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Realizability. An introduction to its categorical side
- A minimalist two-level foundation for constructive mathematics
- First order categorical logic. Model-theoretical methods in the theory of topoi and related categories
- Categorical logic and type theory
- Regular and exact completions
- Locally cartesian closed exact completions
- Some free constructions in realizability and proof theory
- Factorization systems and fibrations
- Modular correspondence between dependent type theories and categories including pretopoi and topoi
- Adjointness in Foundations
- Setoids in type theory
This page was built for publication: Quotient completion for the foundation of constructive mathematics
