Sketches for arithmetic universes

TL;DR

This paper develops a theory of sketches called contexts for arithmetic universes, establishing a correspondence between syntactic models and semantic structures, and constructing free AUs from these contexts.

Contribution

It introduces the notion of contexts for AUs, ensuring a unique isomorphism between non-strict and strict models, and constructs a 2-category of contexts with rich limit properties.

Findings

Every non-strict model is uniquely isomorphic to a strict model.

A concrete construction of free arithmetic universes from contexts is provided.

The 2-category of contexts has finite pie limits and specific pullbacks.

Abstract

A theory of sketches for arithmetic universes (AUs) is developed. A restricted notion of sketch, called here "context", is 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 any context T, a concrete construction is given of the AU AU<T> freely generated by it. A 2-category Con of contexts is defined, with a full and faithful 2-functor to the 2-category of AUs and strict AU-functors, given by T |-> AU<T>. It has finite pie limits, and also all pullbacks of a certain class of "extension" maps. Every object, morphism or 2-cell of Con is a finite structure.