Joyal's arithmetic universe as list-arithmetic pretopos

Maria Emilia Maietti

We explain in detail why the notion of list-arithmetic pretopos should be taken as the general categorical definition for the construction of arithmetic universes introduced by André Joyal to give a categorical proof of Gödel's incompleteness results.

Keywords: Pretopoi, dependent type theory, categorical logic

2000 MSC: 03G30, 03B15, 18C50, 03B20, 03F55

Theory and Applications of Categories, Vol. 24, 2010, No. 3, pp 39-83.

TAC Home