Mathematical Structures in Computer Science


Special Issue: Realizability

Tripos theory in retrospect


ANDREW M. PITTS a1
a1 Cambridge University Computer Laboratory, William Gates Building, J. J. Thomson Avenue, Cambridge, CB3 0FD, U.K.

Abstract

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)