Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels


(0,1)(0,1)-Category theory



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.


Recall that the data of a first-order hyperdoctrine TT consists of a category of terms C TC_T, assumed to have finite products, and a functor

Pred T:C T opHeytAlgPred_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)Pred_T(f))1. We often abbreviate Pred T(f)Pred_T(f) to f *f^\ast, calling it a pullback map. If HH is a Heyting algebra, we let |H|{|H|} denote the underlying set.


A tripos is a first-order hyperdoctrine TT together with, for every object cc of C TC_T, an object PcP c and an element in cPred T(c×Pc)in_c \in Pred_T(c \times P c) such that for any object bb and element pPred T(c×b)p \in Pred_T(c \times b), there exists a map χ:bPc\chi \colon b \to P c with Pred T(1 c×χ)(in c)=pPred_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 cc of C TC_T there is an assigned object P(c)P(c) and an assigned epimorphism

hom(,Pc)|Pred T|(c×)\hom(-, P c) \to {|Pred_T|}(c \times -)

of set-valued functors; the predicate in cin_c is the value of id cid_c under the assigned epimorphism hom(Pc,Pc)|Pred T(c×Pc)|\hom(P c, P c) \to {|Pred_T(c \times P c)|} (_à la_ Yoneda lemma).

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

hom(,P c)hom(,P)(c×) op|Pred T|(c×) op=|Pred T|(c×)\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)(P, in) can be used to generate a generic predicate over cc, as (P c,in c=(eval c) *(in))(P^c, in_c = (eval_c)^\ast(in)), i.e., a generic predicate over cc is obtained by pulling back along the evaluation map eval c:c×P cPeval_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 PcP cP c \to P^c and P cPcP^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 TC_T will indeed often be cartesian closed (frequently taking C T=SetC_T = Set in fact), and triposes are frequently formed in the manner just described, starting with a generic predicate over 11 and pulling it back along the maps eval ceval_c to get a generic predicate over any cc.


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)Hom_{C_T}(Y, X), the posetal reflection of which gives the Heyting algebra P(Y)P(Y). Accordingly, we can specify a tripos with category of terms C TC_T by specifying an object XOb(C T)X \in Ob(C_T) and putting Heyting prealgebra structure on Hom C T(,X)Hom_{C_T}(-, X) in such a way as to yield all the first-order hyperdoctrine structure, with the identity morphism on XX playing the role of the suitably generic predicate.


Coming from toposes

Every topos EE gives rise to a tripos in an obvious way, using C T=EC_T = E and

Pred T=Sub:E opHeytAlg,Pred_T = Sub \colon E^{op} \to HeytAlg,

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

hom(,Ω c)Pred T(c×),\hom(-, \Omega^c) \to Pred_T(c \times -),

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

Coming from complete Heyting algebras

If HH is a complete Heyting algebra, we can take C T=SetC_T = Set, and put

Pred T=hom(,H):Set opHeytAlg.Pred_T = \hom(-, H) \colon Set^{op} \to HeytAlg.

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

Coming from partial combinatory algebras

If AA is a partial combinatory algebra (PCA), we can form a tripos in the following manner. Let C T=SetC_T = Set. For each set XX, one can put a pre-ordering? on P(A) XP(A)^X [here, the P(A)P(A) refers to the actual powerset of AA in SetSet] as follows: given f,gP(A) Xf, g \in P(A)^X, let Hom(f,g)Hom(f, g) be the set of aa in AA such that for all xx in XX and bb in f(x)f(x), aa applied to bb is defined and an element of g(x)g(x). We will of course take fgf \leq g just in case Hom(f,g)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:XYf \colon X \to Y, the pullback map

P(A) f:P(A) YP(A) XP(A)^f \colon P(A)^Y \to P(A)^X

preserves the preorder structure. Now define Pred T(X)Pred_T(X) to be the poset obtained from the preorder P(A) XP(A)^X by posetal reflection. With the help of functional completeness, it may be shown that Pred T(X)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))|Pred T|\hom_{Set}(-, P(A)) \to {|Pred_T|}

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

From triposes to toposes

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

Pred T(X×Y)×Pred T(Y×Z) π X×Y *×π Y×Z * Pred T(X×Y×Y×Z)×Pred T(X×Y×Y×Z) Pred T(X×Y×Y×Z) (1×δ×1) * Pred T(X×Y×Z) 1×!×1 Pred T(X×Z).\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 () :hom(X,Y)hom(Y,X)(-)^\dagger: \hom(X, Y) \to \hom(Y, X) is the evident isomorphism Pred T(X×Y)Pred T(Y×X)Pred_T(X \times Y) \to Pred_T(Y \times X). The opposite of a relation r:XYr \colon X \to Y is r :YXr^\dagger \colon Y \to X, and a relation r:XXr \colon X \to X is symmetric if r =rr^\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:XXr \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 rrrr r \leq r plus symmetry r =rr^\dagger = r. However, for any r:XXr \colon X \to X, it is a consequence of Freyd’s modular law for allegories that rrr rr \leq r r^\dagger r, so that transitivity and symmetry combined yield

rrr r=rrrrrr \leq r r^\dagger r = r r r \leq r r

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

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


Let TT be a tripos, and let Rel TRel_T be the bicategory of relations obtained from TT. Let Split per(Rel T)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)Split_{per}(Rel_T) is a topos.

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

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

Weak triposes

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


A weak tripos is a first-order hyperdoctrine TT together with, for every object cc of C TC_T, an object PcP c and an element in cPred T(c×Pc)in_c \in Pred_T(c \times P c) such that for any object bb and element pPred T(c×b)p \in Pred_T(c \times b), the following sentence is satisfied in the internal logic of TT:

i:b.s:Pc.x:c. c(x,s)p(x,i). \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 BB there is a weak tripos over FinSetFinSet, constructed analogously to the tripos attached to a complete Heyting algebra. (We don’t need BB to be complete since we have only finite sets in the base; but we do need BB to be Boolean rather than just Heyting in order to prove that this is a weak tripos. The resulting topos has BB 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 TT 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 TT gives an embedding of C TC_T as “constant objects” in its associated topos, which is the unit of an adjunction).

A “Synthetic” View of Triposes

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

  1. FF preserves finite limits

  2. every AA in EE appears as subquotient of FIF I for some II in SS

  3. there is a subobject t:TFΣt : T \rightarrowtail F\Sigma such that every mono m:XFIm : X \rightarrowtail F I appears as pullback of tt along FfF f for some (typically not unique) map f:IΣf : I \to \Sigma in SS

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

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

Relation to HH-valued sets

Consider the tripos T=T HT = T_H obtained from a complete Heyting algebra HH (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 XX equipped with a function e:X×XHe \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,zXx, y, z \in X,

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

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

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

    e X(x,x)r(x,y)r(x,y),r(x,y)e Y(y,y)r(x,y).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 rre Xr \leq r \circ e_X means

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

    but since e Xe_X is symmetric and transitive, we have

    r(x,y) xXe X(x,x)r(x,y)= xe X(x,x)e X(x,x)r(x,y) xe X(x,x)e(x,x)e(x,x)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)e X(x,x)r(x, y) \leq e_X(x, x). Similarly we have r(x,y)e(y,y)r(x, y) \leq e(y, y), and these two conditions conversely imply rre Xr \leq r \circ e_X, re Yrr \leq e_Y \circ r, as may be easily checked.

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

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

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

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

The first of these conditions means

r (y,x)r(x,y)=r(x,y)r(x,y)e Y(y,y)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) yYr(x,y)r (y,x)e_X(x, x') \leq \bigvee_{y \in Y} r(x, y) \wedge r^\dagger(y, x')

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

e X(x,x) e X(x,x)e X(x,x) yr(x,y)e X(x,x) yr(x,y)r(x,y) yr(x,y)r (y,x).\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:XYr \colon X \to Y is equivalent to

  • e X(x,x) yYr(x,y)e_X(x, x) \leq \bigvee_{y \in Y} r(x, y)
Theorem (Higgs)

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

Thus all localic toposes arise as toposes of HH-valued sets, where HH is the Heyting algebra of subobjects of 11.

Compare the description by Walters of sheaves over HH 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)\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.


The triposes over SetSet of this form are precisely those for which the preorder imposed on Hom Set(X,P)P XHom_{Set}(X, P) \simeq P^X is the straightforward XX-ary product of the preorder imposed on Hom Set(1,P)PHom_{Set}(1, P) \simeq P, where PP 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 SetSet 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:XXr \colon X \to X is coreflexive if r1 Xr \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 CC to its exact completion C ex/regC_{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.


  • 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 TC_T, i.e., each Pred T(f)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 TC_T is another matter; the original treatment by Pitts assumed more than is actually necessary. Namely, it was assumed that C TC_T is finitely complete and the Beck-Chevalley condition holds for all pullbacks in C TC_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 TC_T.

Revised on February 22, 2018 06:46:00 by Thomas Streicher (2003:71:ce38:3500:4487:549d:8304:20b4)