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.
Julius Hamilton (Jun 18 2024 at 12:44):Thank you.
What then is the category of sets?
I see. Yes, this may be the most immediate issue, since there is no set of all sets.
One solution to this is the introduction of “classes”. As I understand it, the main function of classes is that they act almost like sets, but they avoid Russell’s paradox because they are of a different type, than sets. In other words, we can contain “all sets” in something, as long as it is not a set. Could we then simply claim there are 0-sets, 1-sets, 2-sets, etc., each a distinct type?
Julius Hamilton (Jun 18 2024 at 12:51):Also, if we define “category” as “small category”, is the point that we have implied the existence of large categories in doing so? For example, merely by stating the existence of the category of all small categories, we can ask the question, “What then is ?”
Or, could there be a theory (a collection of formulas) with a model that does not contain any large categories? I mean a restricted form of category theory where large categories technically don’t exist.
Josselin Poiret (Jun 18 2024 at 12:54):Julius Hamilton said:
Thank you.
What then is the category of sets?
I see. Yes, this may be the most immediate issue, since there is no set of all sets.
One solution to this is the introduction of “classes”. As I understand it, the main function of classes is that they act almost like sets, but they avoid Russell’s paradox because they are of a different type, than sets. In other words, we can contain “all sets” in something, as long as it is not a set. Could we then simply claim there are 0-sets, 1-sets, 2-sets, etc., each a distinct type?
Yes! This tower of sets is basically the idea behind Grothendieck universes, and universe hierarchies in type theories like CIC or MLTT used resp. in Coq and Agda.
Josselin Poiret (Jun 18 2024 at 12:55):Julius Hamilton said:
Also, if we define “category” as “small category”, is the point that we have implied the existence of large categories in doing so? For example, merely by stating the existence of the category of all small categories, we can ask the question, “What then is ?”
Or, could there be a theory (a collection of formulas) with a model that does not contain any large categories? I mean a restricted form of category theory where large categories technically don’t exist.
You could develop category theory in the context of "small categories", except that then you cannot talk about some categories that ought to be of interest to you. For example, you cannot talk about , and so presheaf categories are out of reach as well.
Julius Hamilton (Jun 18 2024 at 14:09):Thanks. I’m going to try to keep threads shorter and ask small questions in new threads. I’m marking this as resolved, but feel free to continue the conversation and add more input.
Notification Bot (Jun 18 2024 at 14:09):Julius Hamilton has marked this topic as resolved.
Julius Hamilton (Jun 21 2024 at 02:05):I’m really enjoying this paper so far. 3E7F28C9-2C2E-423A-8732-9B9993B80612.png
B8B53D88-8E40-4268-8C10-75891FE03415.png
8EB5F7C7-BC05-43EB-A346-AF323D673300.png
