Re #7: I’ve just posted something on this at MO.

]]>See here for an old nForum discussion around this.

]]>Thanks very much Thomas! Fantastic that somebody has written up the details of this, I and many people have long wished to see the argument. I’d like to work through it when I get the chance and put some details on the nLab.

]]>Added a reference to

- {#vanDijkOldenziel20} Joost vaan Dijk, Alexander Gietelink Oldenziel,
*Gödel incompleteness through Arithmetic Universes after A. Joyal*, arXiv:2004.10482 (2020). ((abstract)

Thanks!

Gave hyperlinks to you *finite products* and (more importantly) *disjoint coproducts*.

Trying to unwind Maietti’s definition of parameterised list objects, I guess they are just W-types for the non-locally cartesian closed version of the polynomial functor giving list objects. Cockett (JPAA 1990) defines them as initial algebras for the endofunctor $B+A\times (-)$ (for arbitrary $A$ and $B$).

Let me edit that in now… (EDIT: done!)

]]>Alright :-). I guess there’s not much to discuss…

]]>I have added to *arithmetic pretopos* the redirect and the sentence

]]>Maietti proposed that arithmetic pretoposes serve as the

arithmetic universesthat Andre Joyal once suggested to use for discussion of incompleteness theorems.

We have the grey link arithmetic universe at abstract Stone duality, which we may want to redirect to arithmetic pretopos. I only don’t do it, since these are not the same thing (an AU has been defined by Joyal, though no one has seen it), even though Maietti’s proposal is that an arithmetic universe be defined as a list-arithmetic pretopos.

I hope we can flush Joyal’s definition out of the undergrowth…

]]>stub for *arithmetic pretopos*, just to record the reference