Dear Andrej, The initial arithmetic universe is internal to itself in a certain sense. On the one hand, arithmetic universes have enough structure that internally you can do enough algebra to construct initial models of cartesian theories; but on the other hand the theory of arithmetic universes is itself cartesian. Hence the initial arithmetic universe has, internally, an initial arithmetic universe. Joyal has compared them by taking global elements of the internal one and used the difference to capture Goedel's theorem. You'll have to form your own opinion on whether this sense is sensible enough for you. All the best, Steve. On 4 Sep 2013, at 10:23, Andrej Bauer <andrej.bauer@andrej.com> 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
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]