\documentclass[12pt,titlepage]{article} \usepackage{amsmath} \usepackage{mathrsfs} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsthm} \usepackage{mathtools} \usepackage{graphicx} \usepackage{color} \usepackage{ucs} \usepackage[utf8x]{inputenc} \usepackage{xparse} \usepackage{hyperref} %----Macros---------- % % Unresolved issues: % % \righttoleftarrow % \lefttorightarrow % % \color{} with HTML colorspec % \bgcolor % \array with options (without options, it's equivalent to the matrix environment) % Of the standard HTML named colors, white, black, red, green, blue and yellow % are predefined in the color package. Here are the rest. \definecolor{aqua}{rgb}{0, 1.0, 1.0} \definecolor{fuschia}{rgb}{1.0, 0, 1.0} \definecolor{gray}{rgb}{0.502, 0.502, 0.502} \definecolor{lime}{rgb}{0, 1.0, 0} \definecolor{maroon}{rgb}{0.502, 0, 0} \definecolor{navy}{rgb}{0, 0, 0.502} \definecolor{olive}{rgb}{0.502, 0.502, 0} \definecolor{purple}{rgb}{0.502, 0, 0.502} \definecolor{silver}{rgb}{0.753, 0.753, 0.753} \definecolor{teal}{rgb}{0, 0.502, 0.502} % Because of conflicts, \space and \mathop are converted to % \itexspace and \operatorname during preprocessing. % itex: \space{ht}{dp}{wd} % % Height and baseline depth measurements are in units of tenths of an ex while % the width is measured in tenths of an em. \makeatletter \newdimen\itex@wd% \newdimen\itex@dp% \newdimen\itex@thd% \def\itexspace#1#2#3{\itex@wd=#3em% \itex@wd=0.1\itex@wd% \itex@dp=#2ex% \itex@dp=0.1\itex@dp% \itex@thd=#1ex% \itex@thd=0.1\itex@thd% \advance\itex@thd\the\itex@dp% \makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}} \makeatother % \tensor and \multiscript \makeatletter \newif\if@sup \newtoks\@sups \def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}% \def\reset@sup{\@supfalse\@sups={}}% \def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else% \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}% \else \append@sup#2 \@suptrue \fi% \expandafter\mk@scripts\fi} \def\tensor#1#2{\reset@sup#1\mk@scripts#2_/} \def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2% \reset@sup\mk@scripts#3_/} \makeatother % \slash \makeatletter \newbox\slashbox \setbox\slashbox=\hbox{$/$} \def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$} \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa \copy\slashbox \kern-\@tempdima \box\@tempboxa} \def\slash{\protect\itex@pslash} \makeatother % math-mode versions of \rlap, etc % from Alexander Perlis, "A complement to \smash, \llap, and lap" % http://math.arizona.edu/~aprl/publications/mathclap/ \def\clap#1{\hbox to 0pt{\hss#1\hss}} \def\mathllap{\mathpalette\mathllapinternal} \def\mathrlap{\mathpalette\mathrlapinternal} \def\mathclap{\mathpalette\mathclapinternal} \def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}} \def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}} \def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}} % Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2} \let\oldroot\root \def\root#1#2{\oldroot #1 \of{#2}} \renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}} % Manually declare the txfonts symbolsC font \DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n} \SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n} \DeclareFontSubstitution{U}{txsyc}{m}{n} % Manually declare the stmaryrd font \DeclareSymbolFont{stmry}{U}{stmry}{m}{n} \SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n} % Manually declare the MnSymbolE font \DeclareFontFamily{OMX}{MnSymbolE}{} \DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n} \SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n} \DeclareFontShape{OMX}{MnSymbolE}{m}{n}{ <-6> MnSymbolE5 <6-7> MnSymbolE6 <7-8> MnSymbolE7 <8-9> MnSymbolE8 <9-10> MnSymbolE9 <10-12> MnSymbolE10 <12-> MnSymbolE12}{} % Declare specific arrows from txfonts without loading the full package \makeatletter \def\re@DeclareMathSymbol#1#2#3#4{% \let#1=\undefined \DeclareMathSymbol{#1}{#2}{#3}{#4}} \re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46} \re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12} \re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64} \re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6} \re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77} \re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77} \makeatother % \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE \makeatletter \def\Decl@Mn@Delim#1#2#3#4{% \if\relax\noexpand#1% \let#1\undefined \fi \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}} \def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}} \def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}} \Decl@Mn@Open{\llangle}{mnomx}{'164} \Decl@Mn@Close{\rrangle}{mnomx}{'171} \Decl@Mn@Open{\lmoustache}{mnomx}{'245} \Decl@Mn@Close{\rmoustache}{mnomx}{'244} \makeatother % Widecheck \makeatletter \DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}} \def\@widecheck#1#2{% \setbox\z@\hbox{\m@th$#1#2$}% \setbox\tw@\hbox{\m@th$#1% \widehat{% \vrule\@width\z@\@height\ht\z@ \vrule\@height\z@\@width\wd\z@}$}% \dp\tw@-\ht\z@ \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@ \setbox\tw@\hbox{% \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box \tw@}}}% {\ooalign{\box\tw@ \cr \box\z@}}} \makeatother % \mathraisebox{voffset}[height][depth]{something} \makeatletter \NewDocumentCommand\mathraisebox{moom}{% \IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{% \IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}% }{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}% \mathpalette\@temp{#4}} \makeatletter % udots (taken from yhmath) \makeatletter \def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.} \mkern2mu\raise4\p@\hbox{.}\mkern1mu \raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}} \makeatother %% Fix array \newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}} %% \itexnum is a noop \newcommand{\itexnum}[1]{#1} %% Renaming existing commands \newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}} \newcommand{\widevec}{\overrightarrow} \newcommand{\darr}{\downarrow} \newcommand{\nearr}{\nearrow} \newcommand{\nwarr}{\nwarrow} \newcommand{\searr}{\searrow} \newcommand{\swarr}{\swarrow} \newcommand{\curvearrowbotright}{\curvearrowright} \newcommand{\uparr}{\uparrow} \newcommand{\downuparrow}{\updownarrow} \newcommand{\duparr}{\updownarrow} \newcommand{\updarr}{\updownarrow} \newcommand{\gt}{>} \newcommand{\lt}{<} \newcommand{\map}{\mapsto} \newcommand{\embedsin}{\hookrightarrow} \newcommand{\Alpha}{A} \newcommand{\Beta}{B} \newcommand{\Zeta}{Z} \newcommand{\Eta}{H} \newcommand{\Iota}{I} \newcommand{\Kappa}{K} \newcommand{\Mu}{M} \newcommand{\Nu}{N} \newcommand{\Rho}{P} \newcommand{\Tau}{T} \newcommand{\Upsi}{\Upsilon} \newcommand{\omicron}{o} \newcommand{\lang}{\langle} \newcommand{\rang}{\rangle} \newcommand{\Union}{\bigcup} \newcommand{\Intersection}{\bigcap} \newcommand{\Oplus}{\bigoplus} \newcommand{\Otimes}{\bigotimes} \newcommand{\Wedge}{\bigwedge} \newcommand{\Vee}{\bigvee} \newcommand{\coproduct}{\coprod} \newcommand{\product}{\prod} \newcommand{\closure}{\overline} \newcommand{\integral}{\int} \newcommand{\doubleintegral}{\iint} \newcommand{\tripleintegral}{\iiint} \newcommand{\quadrupleintegral}{\iiiint} \newcommand{\conint}{\oint} \newcommand{\contourintegral}{\oint} \newcommand{\infinity}{\infty} \newcommand{\bottom}{\bot} \newcommand{\minusb}{\boxminus} \newcommand{\plusb}{\boxplus} \newcommand{\timesb}{\boxtimes} \newcommand{\intersection}{\cap} \newcommand{\union}{\cup} \newcommand{\Del}{\nabla} \newcommand{\odash}{\circleddash} \newcommand{\negspace}{\!} \newcommand{\widebar}{\overline} \newcommand{\textsize}{\normalsize} \renewcommand{\scriptsize}{\scriptstyle} \newcommand{\scriptscriptsize}{\scriptscriptstyle} \newcommand{\mathfr}{\mathfrak} \newcommand{\statusline}[2]{#2} \newcommand{\tooltip}[2]{#2} \newcommand{\toggle}[2]{#2} % Theorem Environments \theoremstyle{plain} \newtheorem{theorem}{Theorem} \newtheorem{lemma}{Lemma} \newtheorem{prop}{Proposition} \newtheorem{cor}{Corollary} \newtheorem*{utheorem}{Theorem} \newtheorem*{ulemma}{Lemma} \newtheorem*{uprop}{Proposition} \newtheorem*{ucor}{Corollary} \theoremstyle{definition} \newtheorem{defn}{Definition} \newtheorem{example}{Example} \newtheorem*{udefn}{Definition} \newtheorem*{uexample}{Example} \theoremstyle{remark} \newtheorem{remark}{Remark} \newtheorem{note}{Note} \newtheorem*{uremark}{Remark} \newtheorem*{unote}{Note} %------------------------------------------------------------------- \begin{document} %------------------------------------------------------------------- \section*{tripos} \hypertarget{context}{}\subsubsection*{{Context}}\label{context} \hypertarget{type_theory}{}\paragraph*{{Type theory}}\label{type_theory} [[!include type theory - contents]] \hypertarget{category_theory}{}\paragraph*{{$(0,1)$-Category theory}}\label{category_theory} [[!include (0,1)-category theory - contents]] \hypertarget{contents}{}\section*{{Contents}}\label{contents} \noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak \noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak \noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak \noindent\hyperlink{Topos}{Coming from toposes}\dotfill \pageref*{Topos} \linebreak \noindent\hyperlink{Heyt}{Coming from complete Heyting algebras}\dotfill \pageref*{Heyt} \linebreak \noindent\hyperlink{PCA}{Coming from partial combinatory algebras}\dotfill \pageref*{PCA} \linebreak \noindent\hyperlink{from_triposes_to_toposes}{From triposes to toposes}\dotfill \pageref*{from_triposes_to_toposes} \linebreak \noindent\hyperlink{weak_triposes}{Weak triposes}\dotfill \pageref*{weak_triposes} \linebreak \noindent\hyperlink{a_synthetic_view_of_triposes}{A ``synthetic'' view of triposes}\dotfill \pageref*{a_synthetic_view_of_triposes} \linebreak \noindent\hyperlink{relation_to_valued_sets}{Relation to $H$-valued sets}\dotfill \pageref*{relation_to_valued_sets} \linebreak \noindent\hyperlink{relation_to_exact_completion}{Relation to exact completion}\dotfill \pageref*{relation_to_exact_completion} \linebreak \noindent\hyperlink{internal_logic}{Internal logic}\dotfill \pageref*{internal_logic} \linebreak \noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak \hypertarget{idea}{}\subsection*{{Idea}}\label{idea} A \textbf{tripos} is a [[first-order hyperdoctrine|first-order hyperdoctrine with equality]] satisfying an additional property that allows it to interpret [[impredicative logic|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 topos|localic toposes]] and [[realizability topos|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 [[Martin Hyland|Hyland]] work. \hypertarget{definition}{}\subsection*{{Definition}}\label{definition} Recall that the data of a first-order hyperdoctrine $T$ consists of a [[syntactic category|category of terms]] $C_T$, assumed to have [[finite products]], and a [[functor]] \begin{displaymath} Pred_T: C_{T}^{op} \to HeytAlg \end{displaymath} to the category of [[Heyting algebras]], satisfying suitable properties (including [[quantifiers]], i.e., left and right adjoints to ``pullback maps'' $Pred_T(f)$)\footnote{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 \href{http://ncatlab.org/nlab/show/Frobenius+reciprocity#frobenius_laws_and_frobenius_reciprocity_11}{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 \emph{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$.} . We often abbreviate $Pred_T(f)$ to $f^\ast$, calling it a \emph{pullback map}. If $H$ is a Heyting algebra, we let ${|H|}$ denote the underlying set. \begin{defn} \label{}\hypertarget{}{} A \textbf{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.) \end{defn} 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 \emph{[[epimorphism]]} \begin{displaymath} \hom(-, P c) \to {|Pred_T|}(c \times -) \end{displaymath} 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)|}$ (\emph{\`a{} la} [[Yoneda lemma]]). The $in_c$ are called \emph{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 category|cartesian closed]], we then have [[epimorphism|epis]] \begin{displaymath} \hom(-, P^c) \cong \hom(-, P) \circ (c \times -)^{op} \to {|Pred_T|} \circ (c \times -)^{op} = {|Pred_T|}(c \times -) \end{displaymath} 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 category|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$. \begin{remark} \label{}\hypertarget{}{} The surjective natural transformation defining the suitably generic predicate in a tripos of course induces a [[preorder]] (but not necessarily [[poset|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. \end{remark} \hypertarget{examples}{}\subsection*{{Examples}}\label{examples} \hypertarget{Topos}{}\subsubsection*{{Coming from toposes}}\label{Topos} Every [[topos]] $E$ gives rise to a tripos in an obvious way, using $C_T = E$ and \begin{displaymath} Pred_T = Sub \colon E^{op} \to HeytAlg, \end{displaymath} taking an object $e$ to the Heyting algebra of [[subobjects]] $Sub(e)$. Here of course we have not just an epimorphism but an [[isomorphism]] \begin{displaymath} \hom(-, \Omega^c) \to Pred_T(c \times -), \end{displaymath} obtained by pulling back the generic predicate $t \colon 1 \to \Omega$ over $1$ along $eval \colon c \times \Omega^c \to \Omega$. \hypertarget{Heyt}{}\subsubsection*{{Coming from complete Heyting algebras}}\label{Heyt} If $H$ is a [[complete Heyting algebra]], we can take $C_T = Set$, and put \begin{displaymath} Pred_T = \hom(-, H) \colon Set^{op} \to HeytAlg. \end{displaymath} 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$. \hypertarget{PCA}{}\subsubsection*{{Coming from partial combinatory algebras}}\label{PCA} 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 \begin{displaymath} P(A)^f \colon P(A)^Y \to P(A)^X \end{displaymath} 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 \href{http://ncatlab.org/nlab/show/partial+combinatory+algebra#realizability_toposes_11}{here} for details. Notice in this case we have, by construction, an epimorphism between set-valued functors \begin{displaymath} \hom_{Set}(-, P(A)) \to {|Pred_T|} \end{displaymath} and thus we obtain a tripos, called the \emph{realizability tripos} associated with the PCA $A$. \hypertarget{from_triposes_to_toposes}{}\subsection*{{From triposes to toposes}}\label{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-morphism|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)$ [[internal logic|internally]] in the hyperdoctrine: \begin{displaymath} \itexarray{ 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). } \end{displaymath} This gives in fact a [[dagger-category]] [[enriched category|enriched]] in [[poset|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 \emph{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 \emph{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 \emph{[[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 \begin{displaymath} r \leq r r^\dagger r = r r r \leq r r \end{displaymath} in addition to $r r \leq r$, meaning that $r$ is in fact idempotent.) We will be interested in [[split idempotent|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. \begin{theorem} \label{}\hypertarget{}{} 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. \end{theorem} In the case of a \hyperlink{Topos}{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 \hyperlink{PCA}{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 \hyperlink{Heyt}{here}. The description of the resulting topos coincides with that of [[Denis Higgs|Higgs]], in his treatment of localic toposes in terms of Boolean-valued or Heyting-valued set theory (\emph{\`a{} la} Scott and Solovay). \hypertarget{weak_triposes}{}\subsubsection*{{Weak triposes}}\label{weak_triposes} In \hyperlink{Pitts02}{Pitts 2002} it is observed that a somewhat weaker condition than suffices to ensure that the above construction yields a topos. \begin{defn} \label{}\hypertarget{}{} A \textbf{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$: \begin{displaymath} \forall i:b. \exists s:P c. \forall x:c. \in_c(x,s) \Leftrightarrow p(x,i). \end{displaymath} \end{defn} This generalization is not vacuous either. For instance, it is shown in \hyperlink{Pitts02}{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 \emph{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]]). \hypertarget{a_synthetic_view_of_triposes}{}\subsubsection*{{A ``synthetic'' view of triposes}}\label{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 \begin{enumerate}% \item $\Delta_P$ preserves finite limits \item every $A$ in $E$ appears as subquotient of $\Delta_P I$ for some $I$ in $S$ \item 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$ \end{enumerate} 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, \emph{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}$. \hypertarget{relation_to_valued_sets}{}\subsection*{{Relation to $H$-valued sets}}\label{relation_to_valued_sets} Consider the tripos $T = T_H$ obtained from a complete Heyting algebra $H$ (\hyperlink{Heyt}{example 2}), or more exactly the bicategory of relations obtained from this. Let us describe explicitly the bicategory obtained by splitting the PERs: \begin{itemize}% \item 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$, \begin{displaymath} e(x, y) = e(y, x) \end{displaymath} \begin{displaymath} e(x, y) \wedge e(y, z) \leq e(x, z) \end{displaymath} This is also known as an \emph{$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. \item 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'': \begin{displaymath} 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'). \end{displaymath} The condition $r \leq r \circ e_X$ means \begin{displaymath} r(x, y) \leq \bigvee_{x' \in X} e_X(x, x') \wedge r(x', y) \end{displaymath} but since $e_X$ is symmetric and transitive, we have \begin{displaymath} \itexarray{ 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) } \end{displaymath} 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. \end{itemize} Such morphisms $r$ are called \emph{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 \emph{functional} if \begin{itemize}% \item $r \circ r^\dagger \leq 1_{(Y, e_Y)} = e_Y$ (``well-definedness''). \item $e_X = 1_{(X, e_X)} \leq r^\dagger \circ r$ (``totality''); \end{itemize} The first of these conditions means \begin{displaymath} r^\dagger(y, x) \wedge r(x, y') = r(x, y) \wedge r(x, y') \leq e_Y(y, y') \end{displaymath} The second condition means \begin{displaymath} e_X(x, x') \leq \bigvee_{y \in Y} r(x, y) \wedge r^\dagger(y, x') \end{displaymath} 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 \begin{displaymath} \itexarray{ 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'). } \end{displaymath} Thus totality of $r \colon X \to Y$ is equivalent to \begin{itemize}% \item $e_X(x, x) \leq \bigvee_{y \in Y} r(x, y)$ \end{itemize} \begin{theorem} \label{}\hypertarget{}{} 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 [[sheaf|sheaves]] on $H$. \end{theorem} Thus all [[localic topos|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. \begin{remark} \label{}\hypertarget{}{} 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 \hyperlink{PCA}{realizability triposes}. See also [[realizability]]. \end{remark} \hypertarget{relation_to_exact_completion}{}\subsection*{{Relation to exact completion}}\label{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 \begin{itemize}% \item 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 [[allegory|unitary tabular allegory]], which is essentially the same as obtaining a regular category. \item 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 [[regular and exact completions|exact completion]] $C_{ex/reg}$. \end{itemize} \hypertarget{internal_logic}{}\subsection*{{Internal logic}}\label{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]]. \hypertarget{references}{}\subsection*{{References}}\label{references} \begin{itemize}% \item [[Andrew Pitts]], \emph{The theory of [[triposes]]}, thesis, \href{http://www.cl.cam.ac.uk/~amp12/papers/thet/thet.pdf}{pdf} \end{itemize} \begin{itemize}% \item [[Andrew Pitts]], \emph{Tripos theory in retrospect}, \href{http://www.cl.cam.ac.uk/~amp12/papers/tritr/tritr.pdf}{pdf} \end{itemize} \begin{itemize}% \item [[Peter Freyd]] and Andre Scedrov, \emph{Categories, Allegories}, North-Holland 1990. \end{itemize} [[!redirects triposes]] \end{document}