You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Shea Levy (Oct 06 2020 at 10:58):Suppose we're working with category theory defined axiomatically, e.g. some first order system like ETCS. How would we go about formulating the Yoneda lemma in such a system? Of course once we have defined we could just construct a notion of categories internal to and work there, but is there any way to connect Yoneda to the top-level categories we're defining?
Morgan Rogers (he/him) (Oct 06 2020 at 11:25):There is surely always going to be an "external" category, of which the collections of objects and morphisms of your categories will be objects; it will always be a category since we need to define functors as mappings between these.
Shea Levy (Oct 06 2020 at 11:32):[Mod] Morgan Rogers said:
There is surely always going to be an "external" category, of which the collections of objects and morphisms of your categories will be objects; it will always be a category since we need to define functors as mappings between these.
Ah, I think that makes sense! To restate this, any definition of "functor" as a generic concept will require the meta-theory to have some notion of "mapping", which we can then logically see as a category (setting aside whether we can treat it as such within the meta-theory). Is that right?
Morgan Rogers (he/him) (Oct 06 2020 at 11:37):That's what I'm suggesting. I'm not going to claim it's strictly impossible to pull that meta-theoretic category into the theory, but it seems like it will take some significant manipulation.
Morgan Rogers (he/him) (Oct 06 2020 at 11:39):(although this might be exactly the kind of structured "Russell paradox" situation that forces us to resort to talking about universes when we're being very formal)
Shea Levy (Oct 06 2020 at 11:43):Hmm... Now I'm suspecting if we want to keep the meta-theory first order we need something like ETCC... Which as I understand it is an unsolved problem? But either way we'd get out of that, and functors
Fawzi Hreiki (Oct 06 2020 at 11:57):You might want to take a look at the concept of a Yoneda structure
Fawzi Hreiki (Oct 06 2020 at 11:57):https://ncatlab.org/nlab/show/Yoneda+structure
Fawzi Hreiki (Oct 06 2020 at 11:58):The idea is that you directly axiomatise in a 2-category what the Yoneda lemma gives you in the category of categories - namely the free cocompletion of a small category.
Shea Levy (Oct 06 2020 at 11:59):Fawzi Hreiki said:
The idea is that you directly axiomatise in a 2-category what the Yoneda lemma gives you in the category of categories - namely the free cocompletion of a small category.
Awesome, yes! Thank you :)
Fawzi Hreiki (Oct 06 2020 at 11:59):This is quite good https://sites.google.com/site/markwebersmaths/home/yoneda-structures-from-2-toposes
Morgan Rogers (he/him) (Oct 06 2020 at 12:00):Heh so the cost of building in Yoneda for axiomatic 1-categories is that you have to work in a 2-category? I should have seen that coming :joy:
Fawzi Hreiki (Oct 06 2020 at 12:02):That's to be expected I suppose. Although if you're only interested in Cat, you can (kind of) get away with only talking about it 1-categorically. This is because it's self enriched so you get the 2-category structure by looking at the exponential objects (the functor categories)
fosco (Oct 10 2020 at 14:15):[Mod] Morgan Rogers said:
Heh so the cost of building in Yoneda for axiomatic 1-categories is that you have to work in a 2-category? I should have seen that coming :joy:
The axioms for n-level stuff is always at level (n+1), right?
Nathanael Arkor (Oct 10 2020 at 14:19):Fortunately, , so there's a way out.