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.
http://www.tac.mta.ca/tac/volumes/24/3/24-03.dvi
http://www.tac.mta.ca/tac/volumes/24/3/24-03.ps
http://www.tac.mta.ca/tac/volumes/24/3/24-03.pdf
ftp://ftp.tac.mta.ca/pub/tac/html/volumes/24/3/24-03.dvi
ftp://ftp.tac.mta.ca/pub/tac/html/volumes/24/3/24-03.ps