Showing changes from revision #2 to #3:
Added | Removed | Changed
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 of partial recursive functions, and then
construct the effective tripos,
this is the hyperdoctrine over whose predicates over are -valued sets , ordered by if there exists a partial recursive function such that for any and , is defined and contained in .
and then take its category of partial equivalence relations; or
construct the regular category of assemblies over
…
and take its exact completion.
We show how the two are related.
The category of pers
Let be an ordered regular fibration. A partial equivalence relation over the type is relation on that is symmetric and transitive:
A morphism of pers is a relation that satisfies
These form a category . The effective topos is of the effective tripos.
The exact completion
allegory is unitary, tabular.
effective completion is splitting of equivalences .
exact completion is category of maps in this.
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.
…
Revision on November 22, 2012 at 23:38:26 by
Finn Lawler?.
See the history of this page for a list of all contributions to it.