nLab arithmetic pretopos

Idea

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 (cf. van Dijk/Oldenziel 2020); they are used directly as the definition of arithmetic universes e.g. in (Maietti-Vickers 2012).

Related entries

• free monoid

• Gödel's incompleteness theorem

• Lawvere's fixed point theorem

• classifying topos for the theory of objects

References

• 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.

• Joost van Dijk, Alexander Gietelink Oldenziel, Gödel’s Incompleteness after Joyal , arXiv:2004.10482 (2020). (abstract)

• 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)