arithmetic pretopos


Topos Theory

topos theory



Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory





An arithmetic pretopos is a pretopos CC 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×():CCB+ 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)

Revised on January 18, 2017 04:09:13 by Thomas Holder (