Sketches for arithmetic universes

MaRDI QIDQ5224159zbMATH OpenFDO

Authors Steven Vickers

Publication date 19 July 2019

Full work available at URL https://arxiv.org/abs/1608.01559, http://logicandanalysis.org/index.php/jla/article/download/340/152

zbMATH Keywords

generalized spacegeometric theorytopos

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Sketches and generalizations (18C30)

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.

Recommendations

• Arithmetic universes and classifying toposes
• Joyal's arithmetic universes via type theory
• scientific article; zbMATH DE number 5695342
• Reflection into models of finite decidable FP-sketches in an arithmetic universe
• Inside every model of abstract Stone duality lies an arithmetic universe

Cited in

(20)

• Exploring mathematical objects from custom-tailored mathematical universes
• Maximal ideals in countable rings, constructively
• Radical theory of Scott-open filters
• Joyal's arithmetic universes via type theory
• Reflection into models of finite decidable FP-sketches in an arithmetic universe
• Inside every model of abstract Stone duality lies an arithmetic universe
• A sketch theoretical survey. Towards a typology of mathematical structures
• scientific article; zbMATH DE number 4093718 (Why is no real title available?)
• An interpretation of dependent type theory in a model category of locally cartesian closed categories
• The localic compact interval is an Escardó-Simpson interval object
• Fibrations of AU-contexts Beget fibrations of toposes
• On the Weihrauch degree of the additive Ramsey theorem
• Hilbert's tenth problem for term algebras with a substitution operator
• Complemented subsets and Boolean-valued, partial functions
• Defining long words succinctly in FO and MSO
• On the first-order parts of problems in the Weihrauch degrees
• Algorithmically random series
• Ideal presentations and numberings of some classes of effective quasi-Polish spaces
• Lower bounds on () and other properties of -register machines
• Reifying dynamical algebra: maximal ideals in countable rings, constructively

This page was built for publication: Sketches for arithmetic universes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5224159)