5 ms·

Please point out where somebody genuinely puts an effort to found math on category theory? The standard way to do so is set theory, and the more recent hype is

Please point out where somebody genuinely puts an effort to found math on category theory? The standard way to do so is set theory, and the more recent hype is type theory. Category theory in itself is pretty useless. Categories are a bit like graphs in that: they are too general. There are serious mathematical theories using category theory as their language (mostly commutative algebra and whatever it touches) just as there are serious theories using the language of graphs, but in both cases the meat of the math is not in the underlying language.

mbid 9y ago
There are serious efforts to found maths on elementary toposes, which are categories with certain properties. Much the same way that the axioms of ZFC model the properties of sets in terms of the "is element" relation, you can give first order axioms for how the morphisms and objects of an elementary topos behave. Then you may add more axioms to assert that the elementary topos you're talking about is really a category of sets in the sense of ZFC. If you want to research more about this, I can recommend sheaves in geometry and logic by Maclane and Moerdijk. You can also search for "algebraic set theory" and go from there. And btw, type theory is essentially the same thing. The axioms are IMO uglier and more ad-hoc, but there are (some proven, some conjectured) equivalence results.
scentoni 9y ago
https://homotopytypetheory.org/book/ https://homotopytypetheory.org/book/
- lmm 9y ago
  That is a) a great project b) not category theory.
infty 9y ago
>Please point out where somebody genuinely puts an effort to found math on category theory? What about the following: https://ncatlab.org/nlab/show/foundation+of+mathematics#CFM https://ncatlab.org/nlab/show/foundation+of+mathematics#CFM Even if the meat of the math is not in the categorical aspects of a theory, the categorical input can be useful - if nothing else, then as a convenient language.

mbid 9y ago

There are serious efforts to found maths on elementary toposes, which are categories with certain properties. Much the same way that the axioms of ZFC model the properties of sets in terms of the "is element" relation, you can give first order axioms for how the morphisms and objects of an elementary topos behave. Then you may add more axioms to assert that the elementary topos you're talking about is really a category of sets in the sense of ZFC. If you want to research more about this, I can recommend sheaves in geometry and logic by Maclane and Moerdijk. You can also search for "algebraic set theory" and go from there. And btw, type theory is essentially the same thing. The axioms are IMO uglier and more ad-hoc, but there are (some proven, some conjectured) equivalence results.

scentoni 9y ago

https://homotopytypetheory.org/book/ https://homotopytypetheory.org/book/

lmm 9y ago
That is a) a great project b) not category theory.

infty 9y ago

>Please point out where somebody genuinely puts an effort to found math on category theory? What about the following: https://ncatlab.org/nlab/show/foundation+of+mathematics#CFM https://ncatlab.org/nlab/show/foundation+of+mathematics#CFM Even if the meat of the math is not in the categorical aspects of a theory, the categorical input can be useful - if nothing else, then as a convenient language.