Joyal's arithmetic universe as list-arithmetic pretopos
Theory and applications of categories, Tome 24 (2010), pp. 39-83
Cet article a éte moissonné depuis la source Theory and Applications of Categories website
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.
Classification :
03G30, 03B15, 18C50, 03B20, 03F55
Keywords: Pretopoi, dependent type theory, categorical logic
Keywords: Pretopoi, dependent type theory, categorical logic
@article{TAC_2010_24_a2,
author = {Maria Emilia Maietti},
title = {Joyal's arithmetic universe as list-arithmetic pretopos},
journal = {Theory and applications of categories},
pages = {39--83},
year = {2010},
volume = {24},
language = {en},
url = {http://geodesic.mathdoc.fr/item/TAC_2010_24_a2/}
}
Maria Emilia Maietti. Joyal's arithmetic universe as list-arithmetic pretopos. Theory and applications of categories, Tome 24 (2010), pp. 39-83. http://geodesic.mathdoc.fr/item/TAC_2010_24_a2/