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: C-op -> Pos, produces an elementary topos T-P in such a way that the fibration of the subobjects of the topos T-P 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 P-cx : Prd(P)(op) -> Pos on P. The base category has finite limits and embeds into the topos T-P via a functor K: Prd (P) -> T-P determined by the universal property of P-cx and which preserves finite limits. Hence it extends to an exact functor K-ex : (Prd(P))(ex/lex) -> T-P from the exact completion of Prd(P).We characterize the triposes P for which the functor K-ex is an equivalence as those P equipped with a so-called epsilon-operator. We also show that the tripos-to-topos construction need not preserve epsilon-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.