Joyal's arithmetic universe as list-arithmetic pretopos

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 Andre Joyal to give a categorical proof of Godel's incompleteness results. We motivate this definition for three reasons: first, Joyal's arithmetic universes are list-arithmetic 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 Godel'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 Andre Joyal.