ANDREW M. PITTS a1 a1 Cambridge University Computer Laboratory, William Gates Building, J. J. Thomson Avenue, Cambridge, CB3 0FD, U.K.
The notion of tripos (Hyland et
al. 1980; Pitts 1981) 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.
(Received December 7 1999) (Revised August 7 2000)