Where it says U[1, U'_0] = U_0 it should say U_0[1, U'_0] = U_0 On 04/09/13 06:23, Andrej Bauer wrote:
Chatting at a conference, the question came up why there is no (non-trivial) category which is "internal to itself" (interpret this in some sensible sense). And over coffee we thought this must be well known, but not to us. Can somene shed some light on the matter?
With kind regards,
Andrej
Interesting and difficult question. Related to incompletness problems and diagonal arguments. Joyal considered arithmetic universes U (*), and an initial such U_0. (for example, for U = Sets: U_0[1, N] = standard Natural Numbers). Then show that within any arithmetic universe U you can construct internally a U_0. In particular U_0 exist (called U'_0) inside U_0. You have U[1, U'_0] = U_0. With this he proves Godel Incompletness. (*) A pretopos U such that admits free monoids: X \in U, X ---> M(X), in particular, N = M(0). (with this you have primitive recursive arithmetics and construct U_0). I sort of remember also that Penon considered a topos object E' internal to a topos E and such that E[1, E'] = E. It is a challenge to to fill all the technical details and make rigorous sense of all this. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]