Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator
type: Item
instance of: scholarly article
title: Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator
zbMATH Open document ID: 1401.03109
author: Maria Emilia Maietti
author: Fabio Pasquali
author: Giuseppe Rosolini
published in: Tbilisi Mathematical Journal
publication date: 2017-12-08T00:00:00Z
full work available at URL: http://hdl.handle.net/11577/3260512
Mathematics Subject Classification ID: 03G30
Mathematics Subject Classification ID: 18B25
Mathematics Subject Classification ID: 03B15
Mathematics Subject Classification ID: 18C50
zbMATH DE Number: 6816533
MaRDI profile type: Publication
OpenAlex ID: W2768904695
cites work: Equilogical spaces
cites work: Setoids in type theory
cites work: Hilbert's \(\varepsilon{}\)-operator and classical logic
cites work: Hilbert's ϵ‐operator in intuitionistic type theories
cites work: Q3320378
cites work: Some free constructions in realizability and proof theory
cites work: Q4740070
cites work: Regular and exact completions
cites work: Theorie der Numerierungen I
cites work: Categories of continuous functors. I
cites work: Q3995720
cites work: Weak subobjects and the epi-monic completion of a category.
cites work: Q4784090
cites work: Factorization systems and fibrations: toward a fibred Birkhoff variety theorem
cites work: Tripos theory
cites work: Q3671978
cites work: Q3978980
cites work: Adjointness in Foundations
cites work: Q5622402
cites work: Q5642701
cites work: Q4807625
cites work: Q3727946
cites work: A minimalist two-level foundation for constructive mathematics
cites work: Q3552042
cites work: Sheaves in geometry and logic: a first introduction to topos theory
cites work: First order categorical logic. Model-theoretical methods in the theory of topoi and related categories
cites work: Elementary quotient completion
cites work: Quotient completion for the foundation of constructive mathematics
cites work: Unifying exact completions
cites work: Concepts of proof in mathematics, philosophy, and computer science. Based on the Humboldt-Kolleg, Bern, Switzerland, September 9--13, 2013
cites work: A co-free construction for elementary doctrines
cites work: A categorical interpretation of the intuitionistic, typed, first order logic with Hilbert's \(\varepsilon\)-terms
cites work: Tripos theory in retrospect
cites work: The category of equilogical spaces and the effective topos as homotopical quotients
cites work: Data Types as Lattices
cites work: Q3001106
cites work: Q4243759
DOI: 10.1515/TMJ-2017-0106
Recommended article: Remarks on the tripos to topos construction: comprehension, extensionality, quotients and functional-completeness
Recommended article: Hilbert's ϵ‐operator in intuitionistic type theories
Recommended article: Completeness of indexed \(\varepsilon\)-calculus
Recommended article: Triposes, q-toposes and toposes
Recommended article: Q4395643
Recommended article: Q3331889
Recommended article: EXACT COMPLETION AND CONSTRUCTIVE THEORIES OF SETS
Recommended article: Q3717256
Recommended article: Q4271227
Recommended article: Hilbert's \(\varepsilon{}\)-operator and classical logic
description: scientific article; zbMATH DE number 6816533