Triposes, exact completions, and Hilbert's ε-operator.M. E. Maietti, F. Pasquali, G. RosoliniTriposes were introduced as presentations of toposes by J.M.E. Hyland, P.T. Johnstone and A.M. Pitts. They introduced a construction that, from a tripos P:Cop → Pos, produces an elementary topos TP in such a way that the fibration of the subobjects of the topos TP is freely obtained from P. One can also construct the ``smallest'' elementary doctrine made of subobjects which fully extends P, more precisely the free full comprehensive doctrine with comprehensive diagonals Pcx:PredPop → Pos on P. The base category has finite limits and embeds into the topos TP via a functor K:PredP → TP determined by the universal property of Pcx and which preserves finite limits. Hence it extends to an exact functor Kex:(PredP)ex/lex → TP from the exact completion of PredP.We characterize the triposes P for which the functor Kex is an equivalence as those P equipped with a so-called ε-operator. We also show that the tripos-to-topos construction need not preserve ε-operators by producing counterexamples from localic triposes constructed from well-ordered sets. A characterization of the tripos-to-topos construction as a completion to an exact category is instrumental for the results in the paper and we derived it as a consequence of a more general characterization of an exact completion related to Lawvere's hyperdoctrines. Tbilisi Mathematical Journal, Vol. 10(3) (2017), pp. 141-166 |