Finn Lawler thesis outline (Rev #2, changes)

Showing changes from revision #1 to #2: 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.

~~Pages:~~

Chapter 2

regular logic?, regular fibration

allegory, bicategory of relations?

equipment?, cartesian equipment?

…

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$ 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
construct the regular category of assemblies over $\mathbb{N}$
- …
and take its exact completion.

We show how the two are related.

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