Sketches for arithmetic universes

From topos theory comes the idea that continuity is a logical phenomenon, specifically one of geometric logic: a map is continuous if its construction can be carried out within the constructive constraints of geometric logic. This extends the notion of continuity far beyond ordinary topological spaces, as it applies also to maps valued in generalized spaces (toposes) such as the space of sets, and even to bundles as maps taking points to spaces (the fibres). This logical aspect has been brought out explicitly in two topos approaches to quantum foundations.

Categorically, geometric logic is interpreted in Grothendieck toposes. However, a problem is that it has extrinsic infinities (specifically: infinitary disjunctions) supplied by a choice of base topos. This would make it difficult to provide software support for geometric logic. In 1999 I conjectured that, by adding features of a finitary, intrinsic type theory, some infinite disjunctions could be replaced by existential quantification over infinite types such as the natural numbers. Categorically, Grothendieck toposes relative a fixed base would be replaced by Joyal's arithmetic universes (AUs), base-independent.

I shall present my recent work on formalizing the AU-logic using finite sketches. These are restricted to "contexts", defined with the property that every non-strict model is uniquely isomorphic to a strict model. This allows us to reconcile the syntactic, dealt with strictly using universal algebra, with the semantic, in which non-strict models must be considered.

For each context T, there is a classifying AU analogous to a classifying topos, but base-independent, and I shall outline a purely finitary presentation of strict AU-functors and natural transformations between the classifying AUs.

Draft paper at http://arxiv.org/abs/1608.01559