Unifying exact completions

DOI10.1007/S10485-013-9360-5zbMath1386.03074arXiv1212.0966OpenAlexW2166869969MaRDI QIDQ2254599

Giuseppe Rosolini, Maria Emilia Maietti

Publication date: 5 February 2015

Published in: Applied Categorical Structures (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1212.0966

zbMATH Keywords

exact categoryfree constructiontriposelementary existential doctrine

Mathematics Subject Classification ID

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

Related Items (18)

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 ⋮ A topos for continuous logic ⋮ Unnamed Item ⋮ Elementary fibrations of enriched groupoids ⋮ Equilogical spaces and algebras for a double-power monad ⋮ Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator ⋮ Dialectica principles via Gödel doctrines ⋮ A characterization of generalized existential completions ⋮ On categorical structures arising from implicative algebras: from topology to assemblies ⋮ Unnamed Item ⋮ A characterization of those categories whose internal logic is Hilbert's \(\varepsilon\)-calculus ⋮ Elementary doctrines as coalgebras ⋮ On Choice Rules in Dependent Type Theory ⋮ Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice ⋮ The existential completion

Cites Work

• Quotient completion for the foundation of constructive mathematics
• Realizability. An introduction to its categorical side
• A minimalist two-level foundation for constructive mathematics
• Cartesian bicategories. I
• Categorical logic and type theory
• Regular and exact completions
• Some free constructions in realizability and proof theory
• A co-free construction for elementary doctrines
• Exact categories and categories of sheaves
• Factorization systems and fibrations
• Elementary quotient completion
• Tripos theory in retrospect
• Tripos theory
• Adjointness in Foundations
• Setoids in type theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Unifying exact completions