Triposes, exact completions, and Hilbert's \u3b5-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 \u2192 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 \u201csmallest\u201d elementary doctrine made of subobjects which fully extends P, more precisely the free full comprehensive doctrine with comprehensive diagonals Pcx : PrdPop \u2192 Pos on P. The base category has finite limits and embeds into the topos TP via a functor K: PrdP \u2192 TP determined by the universal property of Pcx and which preserves finite limits. Hence it extends to an exact functor Kex: (PrdP )ex/lex \u2192 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 \u3b5-operator. We also show that the tripos-to-topos construction need not preserve \u3b5-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