nLab tripos

Idea

A tripos is a first-order hyperdoctrine with equality satisfying an additional property that allows it to interpret impredicative higher-order logic as well. In particular, every tripos gives rise to a corresponding topos.

The notion of tripos, due to Andrew Pitts, is useful for giving a unified account of two very different classes of toposes: localic toposes and realizability toposes.

The name ‘tripos’ is to be credited to Peter Johnstone, who was the thesis advisor of Pitts. It can be read as an acronym for “Topos Representing Indexed Partially Ordered Set”, but it is memorable also as a pun, referring to a famous examination at Cambridge University where Pitts, Johnstone, and Hyland work.

Definition

Recall that the data of a first-order hyperdoctrine $T$ consists of a category of terms $C_T$, assumed to have finite products, and a functor

$$Pred_T: C_{T}^{op} \to HeytAlg$$

to the category of Heyting algebras, satisfying suitable properties (including quantifiers, i.e., left and right adjoints to “pullback maps” $Pred_T(f)$)¹. We often abbreviate $Pred_T(f)$ to $f^\ast$, calling it a pullback map. If $H$ is a Heyting algebra, we let ${|H|}$ denote the underlying set.

Definition

A tripos is a first-order hyperdoctrine $T$ together with, for every object $c$ of $C_T$, an object $P c$ and an element $in_c \in Pred_T(c \times P c)$ such that for any object $b$ and element $p \in Pred_T(c \times b)$, there exists a map $\chi \colon b \to P c$ with $Pred_T(1_c \times \chi)(in_c) = p$. (N.B.: such $\chi$ need not be unique.)

Another way of phrasing the definition is that to each object $c$ of $C_T$ there is an assigned object $P(c)$ and an assigned epimorphism

$$\hom(-, P c) \to {|Pred_T|}(c \times -)$$

of set-valued functors; the predicate $in_c$ is the value of $id_c$ under the assigned epimorphism $\hom(P c, P c) \to {|Pred_T(c \times P c)|}$ (à la Yoneda lemma).

The $in_c$ are called generic predicates. In particular, put $P = P 1$ and $in = in_1 \in Pred_T(P)$, with corresponding epimorphism $\hom(-, P) \to {|Pred_T|}$. If $C_T$ is cartesian closed, we then have epis

$$\hom(-, P^c) \cong \hom(-, P) \circ (c \times -)^{op} \to {|Pred_T|} \circ (c \times -)^{op} = {|Pred_T|}(c \times -)$$

and in this way the single generic predicate $(P, in)$ can be used to generate a generic predicate over $c$, as $(P^c, in_c = (eval_c)^\ast(in))$, i.e., a generic predicate over $c$ is obtained by pulling back along the evaluation map $eval_c \colon c \times P^c \to P$. (N.B.: this need not reproduce the original generic predicates, but the resulting tripos structure may be compared with the original tripos structure in both directions: there are maps $P c \to P^c$ and $P^c \to P c$, with the generic predicates in the two triposes pulling back to each other along these maps.)

In practice, the category $C_T$ will indeed often be cartesian closed (frequently taking $C_T = Set$ in fact), and triposes are frequently formed in the manner just described, starting with a generic predicate over $1$ and pulling it back along the maps $eval_c$ to get a generic predicate over any $c$.

Remark

The surjective natural transformation defining the suitably generic predicate in a tripos of course induces a preorder (but not necessarily posetal) structure on each $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 Ob(C_T)$ and putting Heyting prealgebra structure on $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.

Examples

Coming from toposes

Every topos $E$ gives rise to a tripos in an obvious way, using $C_T = E$ and

$$Pred_T = Sub \colon E^{op} \to HeytAlg,$$

taking an object $e$ to the Heyting algebra of subobjects $Sub(e)$. Here of course we have not just an epimorphism but an isomorphism

$$\hom(-, \Omega^c) \to Pred_T(c \times -),$$

obtained by pulling back the generic predicate $t \colon 1 \to \Omega$ over $1$ along $eval \colon c \times \Omega^c \to \Omega$.

Coming from complete Heyting algebras

If $H$ is a complete Heyting algebra, we can take $C_T = Set$, and put

$$Pred_T = \hom(-, H) \colon Set^{op} \to HeytAlg.$$

Completeness of $H$ is used to ensure that for each function $f \colon X \to Y$, the Heyting algebra map $Pred_T(f) \colon H^Y \to H^X$ has a left and right adjoint. The identity map $\hom(-, H) \to Pred_T$ is the epimorphism we use to generate the tripos structure, taking of course $(H, 1_H \in H^H)$ as the generic predicate over $1$.

Coming from partial combinatory algebras

If $A$ is a partial combinatory algebra (PCA), we can form a tripos in the following manner. Let $C_T = Set$. For each set $X$, one can put a preorder structure on $P(A)^X$ [here, the $P(A)$ refers to the actual powerset of $A$ in $Set$] as follows: given $f, g \in P(A)^X$, let $Hom(f, g)$ be the set of $a$ in $A$ such that for all $x$ in $X$ and $b$ in $f(x)$, $a$ applied to $b$ is defined and an element of $g(x)$. We will of course take $f \leq g$ just in case $Hom(f, g)$ is inhabited. The relation $\leq$ is reflexive and transitive, by functional completeness for PCA’s. It is straightforward that for a function $f \colon X \to Y$, the pullback map

$$P(A)^f \colon P(A)^Y \to P(A)^X$$

preserves the preorder structure. Now define $Pred_T(X)$ to be the poset obtained from the preorder $P(A)^X$ by posetal reflection. With the help of functional completeness, it may be shown that $Pred_T(X)$ is in fact a Heyting algebra, and we get in this way a hyperdoctrine; see here for details. Notice in this case we have, by construction, an epimorphism between set-valued functors

$$\hom_{Set}(-, P(A)) \to {|Pred_T|}$$

and thus we obtain a tripos, called the realizability tripos associated with the PCA $A$.

From triposes to toposes

Every first-order hyperdoctrine $T = (C_T, Pred_T)$ gives rise to a bicategory of relations, whose objects are the objects of $C_T$ and where 1-cells from $X$ to $Y$ are triples $(X, Y, r \in Pred_T(X \times Y))$, thus thinking of $r$ as a “relation” $r \colon X \to Y$. Thus $\hom(X, Y) = Pred_T(X \times Y)$, and we define hom-composition in the usual way for relational composition, by expressing the formula $(r \circ s)(x, z) = \exists_y r(x, y) \wedge s(y, z)$ internally in the hyperdoctrine:

$$\array{ Pred_T(X \times Y) \times Pred_T(Y \times Z) & \stackrel{\pi_{X \times Y}^\ast \times \pi_{Y \times Z}^\ast}{\to} & Pred_T(X \times Y \times Y \times Z) \times Pred_T(X \times Y \times Y \times Z) \\ & \stackrel{\wedge}{\to} & Pred_T(X \times Y \times Y \times Z) \\ & \stackrel{(1 \times \delta \times 1)^\ast}{\to} & Pred_T(X \times Y \times Z) \\ & \stackrel{\exists_{1 \times ! \times 1}}{\to} & Pred_T(X \times Z). }$$

This gives in fact a dagger-category enriched in posets, where $(-)^\dagger: \hom(X, Y) \to \hom(Y, X)$ is the evident isomorphism $Pred_T(X \times Y) \to Pred_T(Y \times X)$. The opposite of a relation $r \colon X \to Y$ is $r^\dagger \colon Y \to X$, and a relation $r \colon X \to X$ is symmetric if $r^\dagger = r$. In summary, we get an allegory (bicategories of relations being essentially equivalent to unitary pretabular allegories).

In this context, a partial equivalence relation, or PER, may be defined as a symmetric idempotent map $r \colon X \to X$. (In slightly more detail, a partial equivalence relation means we drop reflexivity from the notion of equivalence relation, so we mean transitivity $r r \leq r$ plus symmetry $r^\dagger = r$. However, for any $r \colon X \to X$, it is a consequence of Freyd’s modular law for allegories that $r \leq r r^\dagger r$, so that transitivity and symmetry combined yield

$$r \leq r r^\dagger r = r r r \leq r r$$

in addition to $r r \leq r$, meaning that $r$ is in fact idempotent.)

We will be interested in splitting not all idempotents (as in $Set$-based or $Pos$-based Cauchy completion), but just the symmetric idempotents = PERs, in view of the following theorem.

Theorem

Let $T$ be a tripos, and let $Rel_T$ be the bicategory of relations obtained from $T$. Let $Split_{per}(Rel_T)$ be the bicategory obtained by splitting the PERs. Then the locally discrete bicategory of maps (whose 1-cells are left adjoints or total functional relations) in $Split_{per}(Rel_T)$ is a topos.

In the case of a tripos induced from a topos $T$, this construction yields back $T$, since every partial equivalence relation (as a morphism of $Rel_T$) factors through a suitable subquotient object in $T$.

In the case of a realizability tripos associated with a PCA $A$, this construction yields the realizability topos of $A$. In the particular 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.

Before we undertake a conceptual analysis of this theorem, we give in the next section some details for the tripos attached to a complete Heyting algebra, described here. The description of the resulting topos coincides with that of Higgs?, in his treatment of localic toposes in terms of Boolean-valued or Heyting-valued set theory (à la Scott and Solovay).

Weak triposes

In Pitts 2002 it is observed that a somewhat weaker condition than suffices to ensure that the above construction yields a topos.

Definition

A weak tripos is a first-order hyperdoctrine $T$ together with, for every object $c$ of $C_T$, an object $P c$ and an element $in_c \in Pred_T(c \times P c)$ such that for any object $b$ and element $p \in Pred_T(c \times b)$, the following sentence is satisfied in the internal logic of $T$:

$$\forall i:b. \exists s:P c. \forall x:c. \in_c(x,s) \Leftrightarrow p(x,i).$$

This generalization is not vacuous either. For instance, it is shown in Pitts 2002 that for any infinite Boolean algebra $B$ there is a weak tripos over $FinSet$, constructed analogously to the tripos attached to a complete Heyting algebra. (We don’t need $B$ to be complete since we have only finite sets in the base; but we do need $B$ to be Boolean rather than just Heyting in order to prove that this is a weak tripos. The resulting topos has $B$ as its poset of subterminal objects; it is unknown whether every (not necessarily complete) Heyting algebra can occur as the poset of subterminals in an elementary topos.)

In fact, it also seems unnecessary for the hyperdoctrine $T$ to have equality, since in constructing a topos we equip every object with a new partial equivalence relation to become its “equality”. However, the above construction that goes through a bicategory of relations does rely on the existence of equality, as does the statement of the universal property of this construction (since equality in $T$ gives an embedding of $C_T$ as “constant objects” in its associated topos, which is the unit of an adjunction).

A “synthetic” view of triposes

Every tripos $P$ over a topos $S$ gives rise to a so-called “constant objects” functor $\Delta_P : S \to E$ where $E$ is the topos $S[P]$ induced by $P$. It sends $I$ to $(I,\mathrm{eq}_I)$ where $\mathrm{eq}_I$ is the equality predicate on $I$ in the sense of $P$. For the constant objects functor $\Delta_P : S \to E$ we know that

1. $\Delta_P$ preserves finite limits

2. every $A$ in $E$ appears as subquotient of $\Delta_P I$ for some $I$ in $S$

3. there is a subobject $t : T \rightarrowtail \Delta_P\Sigma$ such that every mono $m : X \rightarrowtail \Delta_P I$ appears as pullback of $t$ along $\Delta_P f$ for some (typically not unique) map $f : I \to \Sigma$ in $S$

and that $P$ is obtained from the subobject fibration of $E$ by change of base along along $\Delta_P$. It follows from observations in Pitts’ thesis that this way triposes over $S$ correspond up to equivalence to functors $F$ from $S$ to toposes $E$ such that $F$ validates the above conditions (1)-(3). Moreover, weak triposes over $S$ correspond to $F$ which validate only conditions (1) and (2). Such $F$ are inverse image parts of localic geometric morphisms iff $F$ has a right adjoint.

Somewhat surprisingly the “chaotic” functor $\nabla$ from $\mathbf{Set}$ to the topos of reflexive graphs is a weak tripos in the above sense. For every non-empty set $I$ the functor $(-)^I : \mathbf{Set} \to \mathbf{Set}$ is a weak tripos. For non-isomorphic finite non-empty sets $I$ and $J$ the functors $(-)^I$ and $(-)^J$ are not equivalent. Thus, nonequivalent weak triposes over $\mathbf{Set}$ can give rise to equivalent toposes. It is an open question whether this is also possible for genuine non-weak triposes over $\mathbf{Set}$.

Relation to $H$-valued sets

Consider the tripos $T = T_H$ obtained from a complete Heyting algebra $H$ (example 2), or more exactly the bicategory of relations obtained from this. Let us describe explicitly the bicategory obtained by splitting the PERs:

• An object in the PER-splitting completion in this case is a set $X$ equipped with a function $e \colon X \times X \to H$ which is symmetric and transitive in the sense described above. This boils down to having, for all elements $x, y, z \in X$,

  $$e(x, y) = e(y, x)$$
  $$e(x, y) \wedge e(y, z) \leq e(x, z)$$

  This is also known as an $H$-valued set. (We do not assume reflexivity, where $\top \leq e(x, x)$ for all $x$.) The function $e$ can be thought of as a measure of equality.

• A morphism from $(X, e_X)$ to $(Y, e_Y)$ is a relation $r \colon X \to Y$, or a function $r \colon X \times Y \to H$, such that $r \circ e_X = r = e_Y \circ r$. (Cf. Karoubi envelope.) The conditions $r \circ e_X \leq r$, $e_Y \circ r \leq r$ mean we have a two-sided “action”:

  $$e_X(x', x) \wedge r(x, y) \leq r(x', y), \qquad r(x, y) \wedge e_Y(y, y') \leq r(x, y').$$

  The condition $r \leq r \circ e_X$ means

  $$r(x, y) \leq \bigvee_{x' \in X} e_X(x, x') \wedge r(x', y)$$

  but since $e_X$ is symmetric and transitive, we have

  $$\array{ r(x, y) & \leq & \bigvee_{x' \in X} e_X(x, x') \wedge r(x', y)\\ & = & \bigvee_{x'} e_X(x, x') \wedge e_X(x', x) \wedge r(x', y)\\ & \leq & \bigvee_{x'} e_X(x, x') \wedge e(x', x) \leq e(x, x) }$$

  so that in fact we have $r(x, y) \leq e_X(x, x)$. Similarly we have $r(x, y) \leq e(y, y)$, and these two conditions conversely imply $r \leq r \circ e_X$, $r \leq e_Y \circ r$, as may be easily checked.

Such morphisms $r$ are called relations between $H$-valued sets. Such relations in $Split_{per}(Rel_T)$ may be composed just as they are in $Rel_T$, and if $r$ is an $H$-valued relation, so is $r^\dagger$. On the other hand, as described at Karoubi envelope, the identity from $(X, e)$ to itself is given by the relation $e$ (clearly the identity $1_X$ doesn’t work!). The result $Split_{per}(Rel_T)$ is also a bicategory of relations (although, as we will eventually see, much more is true).

A relation $r \colon (X, e_X) \to (Y, e_Y)$ between PERs is functional if

• $r \circ r^\dagger \leq 1_{(Y, e_Y)} = e_Y$ (“well-definedness”).

• $e_X = 1_{(X, e_X)} \leq r^\dagger \circ r$ (“totality”);

The first of these conditions means

$$r^\dagger(y, x) \wedge r(x, y') = r(x, y) \wedge r(x, y') \leq e_Y(y, y')$$

The second condition means

$$e_X(x, x') \leq \bigvee_{y \in Y} r(x, y) \wedge r^\dagger(y, x')$$

which certainly implies $e_X(x, x) \leq \bigvee_y r(x, y)$. Conversely, if $e_X(x, x) \leq \bigvee_y r(x, y)$, we have

$$\array{ e_X(x, x') & \leq & e_X(x, x) \wedge e_X(x, x') \\ & \leq & \bigvee_y r(x, y) \wedge e_X(x, x') \\ & \leq & \bigvee_y r(x, y) \wedge r(x', y) \\ & \leq & \bigvee_y r(x, y) \wedge r^\dagger(y, x'). }$$

Thus totality of $r \colon X \to Y$ is equivalent to

• $e_X(x, x) \leq \bigvee_{y \in Y} r(x, y)$

Theorem (Higgs)

For a complete Heyting algebra $H$, the category of $H$-valued sets and functional relations between $H$-valued sets is equivalent to the topos of sheaves on $H$.

Thus all localic toposes arise as toposes of $H$-valued sets, where $H$ is the Heyting algebra of subobjects of $1$.

Compare the description by Walters of sheaves over $H$ as certain types of Cauchy-complete categories enriched in a bicategory. Notice that in that description, the homs are symmetric ($\hom(x, y) = \hom(y, x)$), so that the Cauchy completion or idempotent-splitting completion is the same as the completion by splitting symmetric idempotents.

Remark

The triposes over $Set$ of this form are precisely those for which the preorder imposed on $Hom_{Set}(X, P) \simeq P^X$ is the straightforward $X$-ary product of the preorder imposed on $Hom_{Set}(1, P) \simeq P$, where $P$ is the carrier of the generic predicate; in all other cases, the former is a finer-grained preorder than the latter. Thus, in some sense, triposes over $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 triposes. See also realizability.

Relation to exact completion

As stated above, the topos obtained from a tripos can be described as the category of PERs in the bicategory of relations, and functional relations between them. In different language, the bicategory of PERs or symmetric idempotents and relations between them is a power allegory, and the process of passing to functional relations is just the standard process of passing from power allegories to toposes.

The process of splitting symmetric idempotents in the bicategory of relations can be analyzed into two steps, the first related to taking a regular completion, and the second to taking an exact completion of a regular category. More exactly, they are analogues on the allegorical side of these two types of completion.

The two steps are as follows, starting with a bicategory of relations (or perhaps preferably a framed bicategory of relations). Splitting symmetric idempotents can be obtained by

• First splitting the coreflexive morphisms ($r \colon X \to X$ is coreflexive if $r \leq 1_X$). This results in a tabular bicategory of relations or a unitary tabular allegory, which is essentially the same as obtaining a regular category.

• Then, in the unitary tabular allegory, split equivalence relations. In allegorical language, this results in an effective (unitary tabular) allegory (Freyd-Scedrov, page 213); on the categorical side, it means we pass from a regular category $C$ to its exact completion $C_{ex/reg}$.

Internal logic

Of course, the topos obtained from a tripos has an internal logic. But a tripos itself has an internal logic in which the “types” are the objects of the base category and the propositions are those of the fiber category. In fact, the internal logic of a topos is often presented in a way that actually only makes use of the tripos of subobjects of the topos. The type constructors of this internal logic correspond to objects with universal properties in the base category; so in a general tripos there would be only product types and power types. If the base category is cartesian closed, then the latter would decompose into function types and a type of propositions. However, note that these “functions” are less general than the morphisms in the topos constructed from the tripos; in the internal language of the tripos the latter manifest as anafunctions.

References

• Andrew Pitts, The theory of triposes, thesis, pdf

• Andrew Pitts, Tripos theory in retrospect, pdf

• Peter Freyd and Andre Scedrov, Categories, Allegories, North-Holland 1990.

---

1. In fact one may “quantify” along any term = morphism in the base category $C_T$, i.e., each $Pred_T(f)$ has a left adjoint and a right adjoint, merely if we assume this of projection and diagonal maps and if we assume an appropriate Frobenius law, as one generally does for first-order hyperdoctrines. However, the status of corresponding Beck-Chevalley conditions for pullback diagrams in $C_T$ is another matter; the original treatment by Pitts assumed more than is actually necessary. Namely, it was assumed that $C_T$ is finitely complete and the Beck-Chevalley condition holds for all pullbacks in $C_T$. In actuality, for tripos theory, it is enough to assume Beck-Chevalley only for certain pullbacks which exist by virtue of the finite product structure of $C_T$. ↩