|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-proposition, mere proposition|
|cut rule||composition of classifying morphisms / pullback of display maps||substitution|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|logical conjunction||product||product type|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator, (idemponent) monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
|synthetic mathematics||domain specific embedded programming language|
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 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.
to the category of Heyting algebras, satisfying suitable properties (including quantifiers, i.e., left and right adjoints to “pullback maps” )1. We often abbreviate to , calling it a pullback map. If is a Heyting algebra, we let denote the underlying set.
A tripos is a first-order hyperdoctrine together with, for every object of , an object and an element such that for any object and element , there exists a map with . (N.B.: such need not be unique.)
Another way of phrasing the definition is that to each object of there is an assigned object and an assigned epimorphism
and in this way the single generic predicate can be used to generate a generic predicate over , as , i.e., a generic predicate over is obtained by pulling back along the evaluation map . (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 and , with the generic predicates in the two triposes pulling back to each other along these maps).
In practice, the category will indeed often be cartesian closed (frequently taking in fact), and triposes are frequently formed in the manner just described, starting with a generic predicate over and pulling it back along the maps to get a generic predicate over any .
The surjective natural transformation defining the suitably generic predicate in a tripos of course induces a preorder (but not necessarily posetal) structure on each , the posetal reflection of which gives the Heyting algebra . Accordingly, we can specify a tripos with category of terms by specifying an object and putting Heyting prealgebra structure on in such a way as to yield all the first-order hyperdoctrine structure, with the identity morphism on playing the role of the suitably generic predicate.
Every topos gives rise to a tripos in an obvious way, using and
obtained by pulling back the generic predicate over along .
If is a complete Heyting algebra, we can take , and put
Completeness of is used to ensure that for each function , the Heyting algebra map has a left and right adjoint. The identity map is the epimorphism we use to generate the tripos structure, taking of course as the generic predicate over .
If is a partial combinatory algebra (PCA), we can form a tripos in the following manner. Let . For each set , one can put a pre-ordering? on [here, the refers to the actual powerset of in ] as follows: given , let be the set of in such that for all in and in , applied to is defined and an element of . We will of course take just in case is inhabited. The relation is reflexive and transitive, by functional completeness for PCA’s. It is straightforward that for a function , the pullback map
preserves the preorder structure. Now define to be the poset obtained from the preorder by posetal reflection. With the help of functional completeness, it may be shown that 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
and thus we obtain a tripos, called the realizability tripos associated with the PCA .
Every first-order hyperdoctrine gives rise to a bicategory of relations, whose objects are the objects of and where 1-cells from to are triples , thus thinking of as a “relation” . Thus , and we define hom-composition in the usual way for relational composition, by expressing the formula internally in the hyperdoctrine:
This gives in fact a dagger-category enriched in posets, where is the evident isomorphism . The opposite of a relation is , and a relation is symmetric if . 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 . (In slightly more detail, a partial equivalence relation means we drop reflexivity from the notion of equivalence relation, so we mean transitivity plus symmetry . However, for any , it is a consequence of Freyd’s modular law for allegories that , so that transitivity and symmetry combined yield
in addition to , meaning that is in fact idempotent.)
Let be a tripos, and let be the bicategory of relations obtained from . Let 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 is a topos.
In the case of a tripos induced from a topos , this construction yields back , since every partial equivalence relation (as a morphism of ) factors through a suitable subquotient object in .
In the case of a realizability tripos associated with a PCA , this construction yields the realizability topos of . In the particular case where 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 (a la Scott and Solovay).
Consider the tripos obtained from a complete Heyting algebra (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 equipped with a function which is symmetric and transitive in the sense described above. This boils down to having, for all elements ,
This is also known as an -valued set. (We do not assume reflexivity, where for all .) The function can be thought of as a measure of equality.
A morphism from to is a relation , or a function , such that . (Cf. Karoubi envelope.) The conditions , mean we have a two-sided “action”:
The condition means
but since is symmetric and transitive, we have
so that in fact we have . Similarly we have , and these two conditions conversely imply , , as may be easily checked.
Such morphisms are called relations between -valued sets. Such relations in may be composed just as they are in , and if is an -valued relation, so is . On the other hand, as described at Karoubi envelope, the identity from to itself is given by the relation (clearly the identity doesn’t work!). The result is also a bicategory of relations (although, as we will eventually see, much more is true).
A relation between PERs is functional if
The first of these conditions means
The second condition means
which certainly implies . Conversely, if , we have
Thus totality of is equivalent to
For a complete Heyting algebra , the category of -valued sets and functional relations between -valued sets is equivalent to the topos of sheaves on .
Thus all localic toposes arise as toposes of -valued sets, where is the Heyting algebra of subobjects of .
Compare the description by Walters of sheaves over as certain types of Cauchy-complete categories enriched in a bicategory. Notice that in that description, the homs are symmetric (), so that the Cauchy completion or idempotent-splitting completion is the same as the completion by splitting symmetric idempotents.
The triposes over of this form are precisely those for which the preorder imposed on is the straightforward -ary product of the preorder imposed on , where 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 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.
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 ( is coreflexive if ). 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 to its exact completion .
In fact one may “quantify” along any term = morphism in the base category , i.e., each 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 is another matter; the original treatment by Pitts assumed more than is actually necessary. Namely, it was assumed that is finitely complete and the Beck-Chevalley condition holds for all pullbacks in . 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 . ↩