nLab
tripos

A tripos is a first-order hyperdoctrine with equality satisfying an additional property which is sufficient (but, at least in the original definition by Andrew Pitts, more than necessary) to allow it to interpret impredicative higher-order logic as well (in particular, every tripos gives rise to a corresponding topos). The additional property is particularly easy to state for hyperdoctrines whose category of terms $C_T$ is cartesian closed: such a hyperdoctrine is a tripos just in case it possesses a suitably generic predicate, in the sense that there is a natural transformation from a representable functor ${\mathrm{Hom}}_{C_T}(-,X)$ to $\mid P(-)\mid$ (the “set of predicates on -” functor), all of whose components are surjections (this is of course equivalent, by the Yoneda lemma, to the existence of an element of $\mid P(X)\mid$ for some object $X$ with suitable properties). Note that this notion of “suitably generic predicate” doesn’t require $\mid P(-)\mid$ to actually be representable, but, rather, merely a “quotient” of a representable functor.

By reconstructing from a tripos all the subquotients it can “see” of its given sorts and all the functions it can “see” between them (i.e., moving to its category of partial equivalence relations), one obtains an elementary topos.

The surjective natural transformation defining the suitably generic predicate in a tripos of course induces a preorder (but not necessarily posetal) structure on each ${\mathrm{Hom}}_{C_T}(Y,X)$, the posetal reflection of which gives the Heyting algebra $P(Y)$. Accordingly, we can specify a tripos with category of terms $C_T$ by specifying an object $X\in \mathrm{Ob}(C_T)$ and putting Heyting prealgebra structure on ${\mathrm{Hom}}_{C_T}(-,X)$ in such a way as to yield all the first-order hyperdoctrine structure, with the identity morphism on $X$ playing the role of the suitably generic predicate.

Particularly important is the case of triposes whose category of terms is Set (henceforth, “triposes over $\mathrm{Set}$”). Every complete Heyting algebra $H$ gives rise to a tripos over $\mathrm{Set}$, taking the predicate functor to be $I\mapsto H^I$, with the structure of $H$ providing all the adjoints required for the first-order hyperdoctrine structure. The category of partial equivalence relations for such a tripos will in fact be the category of sheaves over the locale whose frame is given by $H$ (the presentation of localic topoi in terms of $H$-valued partial equivalence relations is due to Higgs?). The triposes over $\mathrm{Set}$ of this form are precisely those for which the preorder imposed on ${\mathrm{Hom}}_{\mathrm{Set}}(Y,X)\simeq X^Y$ is the straightforward $Y$-ary product of the preorder imposed on ${\mathrm{Hom}}_{\mathrm{Set}}(1,X)\simeq X$, where $X$ is the carrier of the suitably generic predicate; in all other cases, the former is a finer-grained preorder than the latter. Thus, in some sense, triposes over $\mathrm{Set}$ are a generalization of the notion of “complete Heyting algebra” taking advantage of the ability to use preorder rather than poset structure to allow for a weakening of the condition of completeness.

An example taking advantage of this generalization is given by realizability?: for any partial combinatory algebra A, one can put a pre-ordering on $P(A{)}^I$ [here, the $P(A)$ refers to the actual powerset of $A$ in $\mathrm{Set}$] as follows: given $f,g\in P(A{)}^I$, let $\mathrm{Hom}(f,g)$ be the set of $a$ in $A$ such that for all $i$ in $I$ and $b$ in $f(i)$, $a$ applied to $b$ is defined and an element of $g(i)$. We will of course take $f\le g$ just in case $\mathrm{Hom}(f,g)$ is inhabited. This turns out to provide Heyting prealgebra structure on $P(A{)}^I$, and, furthermore, even the requisite adjoints to reindexing to equip $P(A)$ as the carrier of the suitably generic predicate of a tripos over $\mathrm{Set}$. This is the realizability tripos for $A$, and its category of partial equivalence relations is the realizability topos for $A$. In the case where $A$ is Kleene's first algebra (the PCA whose elements are natural numbers taken as codes for computer programs taking natural number input and producing natural number output if they halt, with obvious application partial function), this is also called the effective topos.

References

• Andrew M. Pitts, The theory of triposes, thesis, pdf
• Andrew M. Pitts, Tripos theory in retrospect, pdf