# Tripos Theory in Retrospect

#### Andrew M. Pitts,
Cambridge University Computer Laboratory,
Pembroke Street Cambridge CB2 3QG, UK

### Abstract

The notion of `tripos' was motivated by the desire to explain in
what sense Higgs' 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 that has all quotients of
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.

[Slides, paper.]