nLab arithmetic pretopos

Contents

Context

Topos Theory

topos theory

Background

Toposes

Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory

Theorems

Arithmetic

Contents

Idea

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 (cf. van Dijk/Oldenziel 2020); 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.

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

Last revised on May 19, 2020 at 17:26:59. See the history of this page for a list of all contributions to it.