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

Last revised on December 13, 2023 at 17:06:44. See the history of this page for a list of all contributions to it.