The notion of `tripos' was motivated by the desire to explain in what
sense Higg's description of sheaf toposes as H-valued sets and
Hyland's realizability toposes are instances of the same construction.
The construction itself can be seen as the universal solution to the
problem of realizing the predicates of a first order hyperdoctrine as
subobjects in a logos with effective equivalence relations. In this
note it is shown that the resulting logos is actually a topos if and
only if the original hyperdoctrine satisfies a certain comprehension
property. Triposes satisfy this property, but there are examples of
non-triposes satisfying this form of comprehension.