Hostname: page-component-78c5997874-g7gxr Total loading time: 0 Render date: 2024-11-20T05:46:49.764Z Has data issue: false hasContentIssue false

Tripos theory in retrospect

Published online by Cambridge University Press:  06 August 2002

ANDREW M. PITTS
Affiliation:
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.

Type
Research Article
Copyright
© 2002 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)