Hacker News Reader

Comment by Koshkin | Hacker News Reader

Technically, category theory is not more abstract than the rest of (abstract) algebra.

You can derive all other math branches with CT, so yes, it is more abstract. It is "higher level" (in the same sense of programming languages) than other maths.

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.

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.

>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

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.

https://homotopytypetheory.org/book/

That is a) a great project b) not category theory.

No, you can’t. The vast majority of analysis cannot usefully be represented in category theory. You can’t express everything in analysis using morphisms and maps.

When you’re working with structures (algebra, geometry, topology, etc), sure, you can construct them in the language of categories. But that’s very far from “all of math”.

CT exists at the same level as some other "fundamental level" fields of maths like topology and abstract algebra (/algerbraic topology).

It's certainly very abstract and fundamental, but it's definitely not the root field.

You can't derive CT with CT. Though that has nothing to do with your point, just suggesting that we aren't there yet.

You can derive all other math from any Turing complete system. Category theory is no more powerful than that.

Given that turing complete systems are not total, you can actually derive anything, including falsehood, from them. The point being that a general 'turing complete' system is about as useful to use as the basis of mathematics as a banana.

Category theory is not a great basis for mathematics, but at least it's not inconsistent.

Reply on news.ycombinator.com