Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 4 of 4
The page fully formal ETCS is convincing regarding the foundation of the Category of Sets as a first order theory. Good !
What about the formal defintion of FUNCTOR that implies the connection between two categories ?
Usual textbooks are defining a FUNCTOR as two MAPS with some additonnal properties. The first MAP is between two COLLECTIONS of objects. The second MAP is between two COLLECTIONS of arrows. But these usual textbooks never define MAP, neither COLLECTION.
What are the formal systems capable to express the concept of FUNCTOR ? Do those systems rely on set theory ? On some type theory ?
It is possible (may be not handy) to setup a first order theory that formalizes in complete autonomy both the concepts of CATEGORY and FUNCTOR ?
Replace “collection” with “set”, and you get a first-order theory for which Cat is the category of models. When textbooks don’t define “collection” in this context, it’s because there are too many options for how to do things, not because there aren’t enough. It’s mainly to leave things open so the reader can fill in that bit with whatever they prefer and/or is practical at the time.
E.g. while it is typical to talk about categories with a set of objects and a set of morphisms, you might nonetheless want to talk about the “category of all sets” in which case you would need to interpret “collection” as proper class or whatever analogous thing you like to do to deal with the analogous problem that there isn’t a “set of all sets”.
For more foundational questions, category theory contains a theory of sets. Not only is “the category of small sets” rather important, you can also identify sets with discrete categories, and functions of sets with functors of discrete categories. So, if you’re just interested in “what is possible”, it doesn’t really make sense to ask for category theory without set theory, unless you’re doing something esoteric. IMO the history of the subject suggests it is far more practical to take sets (or some analogous notion) as a fundamental notion and construct category theory on top of that, rather than aiming to make categories the fundamental notion.
You may find ETCC to be interesting reading.
Martin-Löf dependent type theory is capable of defining functors between categories without using set theory.
Sorry, I edited my first question … and have replaced it by a refined question. So let me reformulate my reception of your botb replies (Hurkyl and Guest):
Yes, I am interested in foundations.
Yes, I understand your answer (Hurkyl) about COLLECTION, which can be represented by either SETS or CLASSES. Using TYPES is also another option. That is fine with me.
But what about the definition, even axiomatic, of a FUNCTOR ? In textbook, a FUNCTOR is a MAP (two in fact) with special properties. But in turn, how to define a MAP ?
My perception is that to work within categories, in a broad sense, both COLLECTION and MAP are primitive and essential concepts.
In Martin-Löf type theories and alike, I understand that these two concepts are primitively defined through behavior axioms. But in set theory, even the class flavour, the MAP is not primitive, but relies on COLLECTION.
So regarding “clean” foundations for working in category theory (not just the axioms of a CATEGORY), it seems only type theories are satisfactory.
What are your opinions ?
1 to 4 of 4