Contents

topos theory

# Contents

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

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

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

Last revised on October 30, 2017 at 14:09:06. See the history of this page for a list of all contributions to it.