This page is for material relevant to my Ph.D. thesis --- I will try to sketch the important bits here as I write up the document itself. ### Chapter 2 There are two quite different ways to construct the effective topos: we start with the Kleene algebra $(\mathbb{N}, \cdot)$ of partial recursive functions, and then 1. construct the _effective tripos_, * this is the hyperdoctrine $\mathbf{ET}$ over $Set$ whose predicates over $X$ are $\mathbb{N}$-valued sets $X \to P\mathbb{N}$, ordered by $\phi \leq \psi$ if there exists a partial recursive function $\Phi$ such that for any $x \in X$ and $n \in \phi x$, $\Phi n$ is defined and contained in $\psi x$. and then take its category of _partial equivalence relations_; or 1. construct the regular category of _assemblies_ over $\mathbb{N}$ * ... and take its _exact completion_. We show how the two are related. #### The category of pers Let $\mathbf{E} \to \mathbf{B}$ be an ordered [[regular fibration]]. A partial equivalence relation over the type $X \in \mathbf{B}$ is relation $R$ on $X$ that is symmetric and transitive: $$ \begin{aligned} R(x_1, x_2) & \Rightarrow R(x_2, x_1) \\ R(x_1, x_2), R(x_2, x_3) & \Rightarrow R(x_1, x_3) \end{aligned} $$ A morphism $(R, X) \to (S, Y)$ of pers is a relation $F \colon X, Y$ that satisfies $$ \begin{aligned} F(x,y) & \Rightarrow R(x,x) \wedge S(y,y) \\ F(x_1,y_1) \wedge R(x_1, x_2) \wedge S(y_1, y_2) & \Rightarrow F(x_2,y_2) \\ F(x,y_1) \wedge F(x,y_2) & \Rightarrow S(y_1,y_2) \\ R(x,x) & \Rightarrow \exists \upsilon . F(x, \upsilon) \end{aligned} $$ These form a category $Per(\mathbf{E})$. The effective topos is $Per(\mathbf{ET})$. #### The exact completion The category $\mathbf{Asm}$ of assemblies is regular, so the allegory $Rel(\mathbf{Asm})$ is unitary and tabular. Its _effective completion_ is the splitting of equivalences $Rel(\mathbf{Asm})[\check{\mathrm{eqv}}]$: an equivalence is a symmetric monad, and these are the objects of the splitting, while a morphism is a [[nlab:module]]. The exact completion of $\mathbf{Asm}$ is category of maps in this allegory. #### Allegories vs. bicategories of relations A unitary pre-tabular allegory is the same thing as a [[nlab:bicategory of relations]]. This extends to an equivalence of 2-categories. We define a _framed bicategory of relations_ to be a (locally ordered) [[nlab:framed bicategory]] that is a bicategory of relations in which all cartesian-product structure morphisms are 'tight' (or 'representable') maps. Then +-- {: .un_theorem} ###### Theorem The 2-categories of ordered regular fibrations and of framed bicategories of relations are equivalent. =-- +-- {: .proof} ###### Proof **(sketch)**. From a regular fibration $\mathbf{E}$ over $\mathbf{B}$ we construct a bicategory $Matr(\mathbf{E})$, whose objects are those of $\mathbf{B}$ and whose morphisms $X \to Y$ are the objects of $\mathbf{E}(X \times Y)$. Composition is given by the usual composite of relations $$ S R(x z) = [ \exists \upsilon . R(x,\upsilon) \wedge S(\upsilon,z) ] $$ One then shows that this is a framed bicategory of relations, with category of tight maps given by $\mathbf{B}$. Conversely, the inclusion $i \colon TMap(\mathcal{B}) \to \mathcal{B}$ gives rise to a pseudofunctor $Pred(\mathcal{B}) \mathcal{B}(i-, I) \colon TMap(\mathcal{B})^{\mathrm{op}} \to Cat$, where $I$ is the tensor unit of $\mathcal{B}$. It is a regular fibration, and $Pred(-)$ and $Matr(-)$ form an equivalence of 2-categories. =-- +-- {: .un_prop} ###### Proposition The full sub-bicategory of $Rel(\mathbf{Asm})$ on the constant assemblies is equivalent to $Matr(\mathbf{ET})$. =-- +-- {: .un_prop} ###### Proposition $Rel(\mathbf{Asm})$ is equivalent to the splitting $Matr(\mathbf{ET})[\check{\mathrm{crf}}]$ of the coreflexive morphisms in $Matr(\mathbf{ET})$. =--