Perhaps this is not really what you want, though. What I would like to know, related to this, is can there be a non-trivial category internally fibred over itself? This question, like your question, leaves some room to ask just what it means. If we just try to Grothendieck-fiber this category of all categories in NF over itself we meet type problems. A type-level notion of pair will not let us form the set of all pairs of a category and an object in it. Maybe a routine NF trick gets around this, maybe not. I wanted to share this thought, and clarify it for myself, before plunging into the world of NF tricks. best, Colin On Wed, Sep 4, 2013 at 6:11 PM, Colin McLarty <colin.mclarty@case.edu>wrote:
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/ ]