transfinite arithmetic, cardinal arithmetic, ordinal arithmetic
prime field, p-adic integer, p-adic rational number, p-adic complex number
arithmetic geometry, function field analogy
An arithmetic pretopos is a pretopos $C$ with a parameterized natural numbers object. A list-arithmetic pretopos is a pretopos with all parameterized list objects (Maietti 10, 2.6).
Using the (equivalent) definition given in Cockett 1990, a parameterized list object is a W-type for the polynomial functor $B+ A\times(-)\colon C\to C$. This definition makes sense since a pretopos has finite products and disjoint coproducts (here denoted “$+$”).
Discussion via its internal language, which is a dependent type theory… (Maietti 05, Maietti 10, p.6).
Maietti (05,10) proposed that list-arithmetic pretoposes serve as the arithmetic universes that André Joyal (cf. Joyal 05) once suggested to use for discussion of incompleteness theorems; they are used directly as the definition of arithmetic universes e.g. in (Maietti-Vickers 2012).
Robin Cockett, List-arithmetic distributive categories: Locoi, JPAA 66 no.1 (1990) pp.1-29.
Robin Cockett, Finite objects in a locos, JPAA 116 (1997) pp.169-183.
André Joyal, The Gödel incompleteness theorem, a categorical approach , (abstract) Amiens 2005, Cah. Top. Géom. Diff. Cat. 46 no.3 (2005) p.202. (numdam)
Maria Maietti, Reflection Into Models of Finite Decidable FP-sketches in an Arithmetic Universe , ENTCS 122 (2005) pp.105-126.
Maria Maietti, Modular correspondence between dependent type theories and categories including pretopoi and topoi, Mathematical Structures in Computer Science 15 no.6 (2005) pp.1089-1149. (draft)
Maria Maietti, Joyal’s arithmetic universe as list-arithmetic pretopos , TAC 24 no.3 (2010) pp.39-83. (abstract)
M. E. Maietti, S. Vickers, An induction principle for consequence in arithmetic universes , JPAA 216 (2012) pp.2049-2067. (draft)
Paul Taylor, Inside Every Model of Abstract Stone Duality Lies an Arithmetic Universe , ENTCS 122 (2005) pp.247–296.
Steve Vickers, Sketches for arithmetic universes , arXiv:1608.0159 (2016). (link)
Steve Vickers, Arithmetic universes and classifying toposes , arXiv:1701.04611 (2017). (link)