Joyal's arithmetic universe as list-arithmetic pretopos
Maria Emilia Maietti · Theory and applications of categories · 2010
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.We motivate this definition for three reasons: first, Joyal's arithmetic universes are listarithmetic pretopoi; second, the initial arithmetic universe among Joyal's constructions is equivalent to the initial list-arithmetic pretopos; third, any list-arithmetic pretopos enjoys the existence of free internal categories and diagrams as required to prove Gödel's incompleteness.In doing our proofs we make an extensive use of the internal type theory of the categorical structures involved in Joyal's constructions.The definition of list-arithmetic pretopos is equivalent to the general one that I came to know in a recent talk by André Joyal.