4 ms·

Just a cautionary note - category theory has seemingly been at "There's tremendous potential here! We just need to find a big win to make that clear to everyon

Just a cautionary note - category theory has seemingly been at "There's tremendous potential here! We just need to find a big win to make that clear to everyone else..." for quite a few years now.

minkowski 6y ago
This is rather uncharitable. Category theory is an essential part of the vocabulary of 20th-century mathematics. Large swaths of algebra, topology, geometry, and logic are fairly inextricably formulated in this language. Similarly, it seems irreplaceable for certain parts of programming language theory (arguably due to its connection to mathematical logic). There's certainly a community trying to bring a category-theoretic approach into other fields such as statistics, economics, or other areas of computer science, but it's too early to say it's been "quite a few years".
- T-A 6y ago
  I think parent meant big wins in physics, where the search started well over a decade ago. See e.g. the dates of the references here: https://en.wikipedia.org/wiki/Categorical_quantum_mechanics#References https://en.wikipedia.org/wiki/Categorical_quantum_mechanics#...
  - GoblinSlayer 6y ago
    QM is just linear algebra, no need to turn it into Haskell.
Kednicma 6y ago
I'm obliged, I suppose, to list off a few big wins. From the 50s and 60s, we have classic theorems which use abstract nonsense to generalize big statements about entire classes of objects, like Freyd's adjoint functor theorem [0], Yoneda's lemma [1], and Lawvere's fixed-point theorem [2]. Yoneda's lemma is the slogan that "an object is equivalent to the arrows coming/leaving it", but formal. Lawvere's theorem is a deep and permanent generalization of Gödel, Tarski, Turing, et al. on incompleteness and undecideability. Starting in the 60s and continuing to the present, there's been a theme of exploring category theory as a prime foundation for maths. There's been complete foundations like the Elementary Theory of the Category of Categories (ETCC) [3], and also much smaller but pointed presentations that focus on just simplifying set theory. I like [4] in particular. On a deeper level, in terms of structure and philosophy, the entire existence of homotopy type theory (HoTT) relies on categorical presentations and memes. HoTT is, more than any other type theory, an investigation into what equivalence means, and it dovetails wonderfully with 2-category theory and the understanding that algebraic laws can be transformed into transformations. [0] https://en.wikipedia.org/wiki/Formal_criteria_for_adjoint_functors https://en.wikipedia.org/wiki/Formal_criteria_for_adjoint_fu... [1] https://en.wikipedia.org/wiki/Yoneda_lemma https://en.wikipedia.org/wiki/Yoneda_lemma [2] http://tac.mta.ca/tac/reprints/articles/15/tr15.pdf http://tac.mta.ca/tac/reprints/articles/15/tr15.pdf [3] https://ncatlab.org/nlab/show/ETCC https://ncatlab.org/nlab/show/ETCC [4] https://arxiv.org/abs/1212.6543 https://arxiv.org/abs/1212.6543
- spekcular 6y ago
  Those aren't really "big wins" though. To most mathematicians, generalizations and abstraction are only interesting insofar as they are useful, and I don't see any results there someone working in mainstream mathematics would or should care about. (Obviously the Yoneda lemma is used in algebraic topology and geometry, but that's the odd one out on your list, and you don't really need categorical language to state the interesting examples.) Also, EETC/HoTT are basically junk, as explained in detail by Harvey Friedman in various postings on the foundations of math mailing list. We already have a perfectly good foundation for mathematics and EETC/HoTT don't improve on it in any way (and in fact are worse in many respects).
  - Kednicma 6y ago
    Friedman and Simpson are, unfortunately, dinosaurs who don't grok categorical concepts. This became clear on the FOM list when Pratt and other abstract algebraists who know category theory but do not depend on it were able to pry apart the problem. Friedman and Simpson deny that certain mathematical objects exist and are equivalent to each other, and while I won't begrudge them their nearsight due to spending so much time with weak/reverse maths, I won't excuse the mistakes. I had to go find a blow-by-blow of the drama because it's good. Simpson cannot imagine topoi which don't implement standard set theory [3]. Friedman demonstrates a total misunderstanding of sets vs. categories [4]. McLarty and Feferman claim that categorical FOM make sense once one is used to categories [1]. Finally, the truth is laid bare: Friedman and Simpson simply don't agree with us on whether categorical logic is philosophically valid [2]. For more on this perspective, check out Pratt's take on Yoneda's lemma [0]. (An interesting aside: Simpson is an Objectivist who hates postmodernism! I wonder if this is part of what causes them to reject topos theory, where there are many different logics and collections, with a single barren plain Boolean set theory?) [0] http://boole.stanford.edu/pub/yon.pdf http://boole.stanford.edu/pub/yon.pdf [1] https://cs.nyu.edu/pipermail/fom/1998-March/001309.html https://cs.nyu.edu/pipermail/fom/1998-March/001309.html [2] https://cs.nyu.edu/pipermail/fom/1998-March/001467.html https://cs.nyu.edu/pipermail/fom/1998-March/001467.html [3] https://cs.nyu.edu/pipermail/fom/1998-January/000782.html https://cs.nyu.edu/pipermail/fom/1998-January/000782.html [4] https://cs.nyu.edu/pipermail/fom/1998-January/000835.html https://cs.nyu.edu/pipermail/fom/1998-January/000835.html

Just a cautionary note - category theory has seemingly been at "There's tremendous potential here! We just need to find a big win to make that clear to everyone else..." for quite a few years now.

minkowski 6y ago

This is rather uncharitable. Category theory is an essential part of the vocabulary of 20th-century mathematics. Large swaths of algebra, topology, geometry, and logic are fairly inextricably formulated in this language. Similarly, it seems irreplaceable for certain parts of programming language theory (arguably due to its connection to mathematical logic). There's certainly a community trying to bring a category-theoretic approach into other fields such as statistics, economics, or other areas of computer science, but it's too early to say it's been "quite a few years".

T-A 6y ago
I think parent meant big wins in physics, where the search started well over a decade ago. See e.g. the dates of the references here: https://en.wikipedia.org/wiki/Categorical_quantum_mechanics#References https://en.wikipedia.org/wiki/Categorical_quantum_mechanics#...
- GoblinSlayer 6y ago
  QM is just linear algebra, no need to turn it into Haskell.

Kednicma 6y ago

I'm obliged, I suppose, to list off a few big wins. From the 50s and 60s, we have classic theorems which use abstract nonsense to generalize big statements about entire classes of objects, like Freyd's adjoint functor theorem [0], Yoneda's lemma [1], and Lawvere's fixed-point theorem [2]. Yoneda's lemma is the slogan that "an object is equivalent to the arrows coming/leaving it", but formal. Lawvere's theorem is a deep and permanent generalization of Gödel, Tarski, Turing, et al. on incompleteness and undecideability. Starting in the 60s and continuing to the present, there's been a theme of exploring category theory as a prime foundation for maths. There's been complete foundations like the Elementary Theory of the Category of Categories (ETCC) [3], and also much smaller but pointed presentations that focus on just simplifying set theory. I like [4] in particular. On a deeper level, in terms of structure and philosophy, the entire existence of homotopy type theory (HoTT) relies on categorical presentations and memes. HoTT is, more than any other type theory, an investigation into what equivalence means, and it dovetails wonderfully with 2-category theory and the understanding that algebraic laws can be transformed into transformations. [0] https://en.wikipedia.org/wiki/Formal_criteria_for_adjoint_functors https://en.wikipedia.org/wiki/Formal_criteria_for_adjoint_fu... [1] https://en.wikipedia.org/wiki/Yoneda_lemma https://en.wikipedia.org/wiki/Yoneda_lemma [2] http://tac.mta.ca/tac/reprints/articles/15/tr15.pdf http://tac.mta.ca/tac/reprints/articles/15/tr15.pdf [3] https://ncatlab.org/nlab/show/ETCC https://ncatlab.org/nlab/show/ETCC [4] https://arxiv.org/abs/1212.6543 https://arxiv.org/abs/1212.6543

spekcular 6y ago
Those aren't really "big wins" though. To most mathematicians, generalizations and abstraction are only interesting insofar as they are useful, and I don't see any results there someone working in mainstream mathematics would or should care about. (Obviously the Yoneda lemma is used in algebraic topology and geometry, but that's the odd one out on your list, and you don't really need categorical language to state the interesting examples.) Also, EETC/HoTT are basically junk, as explained in detail by Harvey Friedman in various postings on the foundations of math mailing list. We already have a perfectly good foundation for mathematics and EETC/HoTT don't improve on it in any way (and in fact are worse in many respects).
- Kednicma 6y ago
  Friedman and Simpson are, unfortunately, dinosaurs who don't grok categorical concepts. This became clear on the FOM list when Pratt and other abstract algebraists who know category theory but do not depend on it were able to pry apart the problem. Friedman and Simpson deny that certain mathematical objects exist and are equivalent to each other, and while I won't begrudge them their nearsight due to spending so much time with weak/reverse maths, I won't excuse the mistakes. I had to go find a blow-by-blow of the drama because it's good. Simpson cannot imagine topoi which don't implement standard set theory [3]. Friedman demonstrates a total misunderstanding of sets vs. categories [4]. McLarty and Feferman claim that categorical FOM make sense once one is used to categories [1]. Finally, the truth is laid bare: Friedman and Simpson simply don't agree with us on whether categorical logic is philosophically valid [2]. For more on this perspective, check out Pratt's take on Yoneda's lemma [0]. (An interesting aside: Simpson is an Objectivist who hates postmodernism! I wonder if this is part of what causes them to reject topos theory, where there are many different logics and collections, with a single barren plain Boolean set theory?) [0] http://boole.stanford.edu/pub/yon.pdf http://boole.stanford.edu/pub/yon.pdf [1] https://cs.nyu.edu/pipermail/fom/1998-March/001309.html https://cs.nyu.edu/pipermail/fom/1998-March/001309.html [2] https://cs.nyu.edu/pipermail/fom/1998-March/001467.html https://cs.nyu.edu/pipermail/fom/1998-March/001467.html [3] https://cs.nyu.edu/pipermail/fom/1998-January/000782.html https://cs.nyu.edu/pipermail/fom/1998-January/000782.html [4] https://cs.nyu.edu/pipermail/fom/1998-January/000835.html https://cs.nyu.edu/pipermail/fom/1998-January/000835.html