Finn Lawler thesis outline (Rev #4, changes)

Showing changes from revision #3 to #4: Added | ~~Removed~~ | ~~Chan~~ged

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

construct the effective tripos,
- this is the hyperdoctrine ~~over~~ $Set ET$ ~~Set~~ \mathbf{ET} ~~whose~~ ~~predicates~~ over $X Set$ X Set ~~are~~ whose predicates over $ℕ X$ ~~\mathbb{N}~~ X ~~-valued~~ ~~sets~~ are $X \to P ℕ$ X \mathbb{N} ~~\to~~ ~~P\mathbb{N}~~ , -valued ~~ordered~~ sets by $ϕ X \leq \to ψ P ℕ$ ~~\phi~~ X ~~\leq~~ \to ~~\psi~~ P\mathbb{N} , if ordered ~~there~~ by ~~exists~~ a ~~partial~~ ~~recursive~~ ~~function~~ $Φ ϕ \leq ψ$ ~~\Phi~~ \phi \leq \psi ~~such~~ if ~~that~~ there ~~for~~ exists ~~any~~ a partial recursive function $x Φ \in X$ x \Phi ~~\in~~ X ~~and~~ such that for any $n \in ϕ x \in X$ n ~~\in~~ ~~\phi~~ x \in X , and $Φ n \in ϕ x$ ~~\Phi~~ n \in \phi x , is ~~defined~~ ~~and~~ ~~contained~~ in $ψ Φ x n$ ~~\psi~~ \Phi x n is defined and contained in $\psi x$ .
and then take its category of partial equivalence relations; or
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 (E \to B)$ ~~Per(\mathbf{E}~~ Per(\mathbf{E}) ~~\to~~ ~~\mathbf{B})~~. The effective topos is $Per (ET)$ ~~Per~~ Per(\mathbf{ET}) . of ~~the~~ ~~effective~~ ~~tripos.~~

The exact completion

allegory $Rel(\mathbf{Asm})$ is unitary, tabular.

effective completion is splitting of equivalences $Rel(\mathbf{Asm})[\check{\mathrm{eqv}}]$ .

exact completion is category of maps in this.

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

Theorem

The 2-categories of ordered regular fibrations and of framed bicategories of relations are equivalent.

…

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.

Proposition

The full sub-bicategory of $Rel(\mathbf{Asm})$ on the constant assemblies is equivalent to $Matr(\mathbf{ET})$ .

Proposition

$Rel(\mathbf{Asm})$ is equivalent to the splitting $Matr(\mathbf{ET})[\check{\mathrm{crf}}]$ of the coreflexive morphisms in $Matr(\mathbf{ET})$ .

Revision on November 23, 2012 at 01:35:19 by Finn Lawler?. See the history of this page for a list of all contributions to it.