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.]