Dear Andrej, To begin, consider a category C with finite limits. Suppose C has an internal category U such that the externalisation of U as a C-indexed category (or category fibred over C) is equivalent to the self-indexing of C. Since U is locally small as a C-indexed category, the self-indexing of C has the same property, so we deduce that C is locally cartesian closed. We have a universal fibration el U -> ob U (by restricting the fibration mor U -> ob U x ob U), so it follows that every object X admits a monomorphism X -> el U. Now, if we add the assumption that C (or U) is well-powered as a C-indexed category, then C must be an elementary topos. But then the existence of el U implies that the internal logic of C is inconsistent, so C must be the degenerate topos. It appears we need to relax the notion of "internal" to get something more reasonable. Here is one idea: instead of taking just one internal category, we take a (large) filtered diagram of them. More precisely, let U be a diagram of shape J in the category of internal categories in C, where J is filtered and the transition functors are (internally) fully faithful, and define a C-indexed category whose fibre over X is the (external) category colim Hom(X, U). When C is an elementary topos, there exists a diagram U such that this construction yields a C-indexed category that is equivalent to the self-indexing of C: take J to be the poset of all finite subsets of ob C, and take as the internal category at a finite set {X_1, ..., X_n} of objects of C to be the internal full subcategory whose objects are the subobjects of the power object P(X_1 + ... + X_n). In the converse direction, if such a diagram of internal categories exists, then one can still deduce (from the condition on transition functors) that the self-indexing of C is locally small. But perhaps there is a strange locally cartesian closed category out there that is self-internal in the naive sense. Best regards, -- Zhen Lin On 4 September 2013 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/ ]