Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator

DOI10.1515/TMJ-2017-0106zbMath1401.03109OpenAlexW2768904695MaRDI QIDQ1683372

Maria Emilia Maietti, Fabio Pasquali, Giuseppe Rosolini

Publication date: 8 December 2017

Published in: Tbilisi Mathematical Journal (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/11577/3260512

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Topoi (18B25) Categorical semantics of formal languages (18C50)

Related Items (10)

Dialectica logical principles ⋮ On a generalization of equilogical spaces ⋮ Dialectica principles via Gödel doctrines ⋮ A characterization of generalized existential completions ⋮ On categorical structures arising from implicative algebras: from topology to assemblies ⋮ Categories of partial equivalence relations as localizations ⋮ A characterization of those categories whose internal logic is Hilbert's \(\varepsilon\)-calculus ⋮ Elementary doctrines as coalgebras ⋮ A PREDICATIVE VARIANT OF HYLAND’S EFFECTIVE TOPOS ⋮ The existential completion

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
• Unnamed Item
• Concepts of proof in mathematics, philosophy, and computer science. Based on the Humboldt-Kolleg, Bern, Switzerland, September 9--13, 2013
• Quotient completion for the foundation of constructive mathematics
• The category of equilogical spaces and the effective topos as homotopical quotients
• A categorical interpretation of the intuitionistic, typed, first order logic with Hilbert's \(\varepsilon\)-terms
• A minimalist two-level foundation for constructive mathematics
• Sheaves in geometry and logic: a first introduction to topos theory
• Hilbert's \(\varepsilon{}\)-operator and classical logic
• First order categorical logic. Model-theoretical methods in the theory of topoi and related categories
• Regular and exact completions
• Weak subobjects and the epi-monic completion of a category.
• Equilogical spaces
• Some free constructions in realizability and proof theory
• A co-free construction for elementary doctrines
• Unifying exact completions
• Categories of continuous functors. I
• Factorization systems and fibrations
• Elementary quotient completion
• Tripos theory in retrospect
• Tripos theory
• Theorie der Numerierungen I
• Data Types as Lattices
• Adjointness in Foundations
• Hilbert's ϵ‐operator in intuitionistic type theories
• Setoids in type theory

This page was built for publication: Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator