Triposes, exact completions, and Hilbert's ε-operator

Triposes 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 : PrdPop → Pos on P. The base category has finite limits and embeds into the topos TP via a functor K: PrdP → TP determined by the universal property of Pcx and which preserves finite limits. Hence it extends to an exact functor Kex: (PrdP )ex/lex → TP from the exact completion of PrdP . 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.