A category internal to itself
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/ ]
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/ ]
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/ ]
In the set theory New Foundations (NF) using Quine's type-level pairing (so a pair has the same type in a stratification as its components) you can define small categories and small functors the usual way. Then, just as there is a set of all sets, there is a small category of all small categories. This is not a tautology. You have to verify a few things. Notably, in this context there is a set of all small functors because there is a set of all functions (yet the category of sets is not cartesian closed, because it lacks evaluation functions). Since a function is stratified at the same level as its domain and codomain sets there is no problem defining domain, codomain, composition, and identity-assigning functors for this category. This category is internal to itself. This example is even left exact. But it is not cartesian closed. Of course the consistency of NF is not settled. But I think everyone supposes it is equiconsistent with some more usual set theory (likely with ETCS). best, Colin On Wed, Sep 4, 2013 at 5:23 AM, 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/ ]
There are some forms of set theory in which there are restrictions on the forms of comprehension allowed, and as a result there is a set of all sets. Quine's New Foundations is one of these. It has a simple restriction on the forms of predicates allowed in comprehensions. Put simply this is that you can assign (integer) levels to the variables in the formula so that x e y only occurs when y is at the level immediately above x. This means that in models of this set theory there is also an internal category of all sets. best Edmund On 4 Sep 2013, at 10: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
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
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/ ]
A comment on Zhen Lin's reply to 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 ...
Just to remark that there is no need to add any assumption here. If a locally cartesian closed category has a "universal fibration" as you call it (called "generic family" in the reference below), then it is degenerate. This appears in: Pitts, Andrew M.; Taylor, Paul. A note on Russell's paradox in locally Cartesian closed categories. Studia Logica 48 (1989), no. 3, 377?387. (MR1059248) With best wishes, Alex -- Alex Simpson, LFCS, School of Informatics, Univ. of Edinburgh, UK Email: Alex.Simpson@ed.ac.uk Tel: +44 (0)131 650 5113 Web: http://homepages.inf.ed.ac.uk/als Fax: +44 (0)131 651 1426 -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
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.
Excellent observation! Thus C is a model for Martin-Loef type theory with Type : Type (as interpreted by U). It is known since Girard's paradox from 1970 that this type theory is inconsistent, i.e. that every type is inhabited. Thus, in particular, all identity types are inhabited which renders C trivial. For a more categorical account of the inconcistency of type theory with Type:Type see A note on Russell's paradox in locally cartesian closed categories Andrew M. Pitts & Paul Taylor Studia Logica 48 (3):377 - 387 (1989) which is much simpler than Girard's original proof. But I don't understand some of your subsequent arguments.
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.
why? and if so what is the point? in a topos for every object X there is a mono 0 -> X
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.
You can't derive wellpoweredness because C lacks (nice) quotients, isn't it? Moreover, for showing that a topos with a universal family is trivial you need something like a proof that Type:Type is inconsistent. But I think that quite correctly you spotted the inconsistency `a la Russell, namely that there is not a set of all sets (or a type of all types). Thomas Streicher [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (8)
-
Alex Simpson -
Andrej Bauer -
Colin McLarty -
Edmund Robinson -
Eduardo J. Dubuc -
Steve Vickers -
Thomas Streicher -
Zhen Lin Low