Finn Lawler empty 6 (Rev #2, changes)

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

2. 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:

A morphism $(R, X) \to (S, Y)$ of pers is a relation $F \colon X, Y$ that satisfies

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 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 bicategory of relations. This extends to an equivalence of 2-categories.

We define a framed bicategory of relations to be a (locally ordered) framed bicategory that is a bicategory of relations in which all cartesian-product structure morphisms are ‘tight’ (or ‘representable’) maps. Then