Hostname: page-component-74656f9884-npj9w Total loading time: 0 Render date: 2026-11-09T14:03:03.165Z 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.
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

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.

Information

Type
Research Article
Copyright
© 2002 Cambridge University Press