3 ms·

tl;dr seems to be that some mathematicians think Jacob Lurie's work on infinity categories points to a better concept of equivalence than normal equivalence rel

tl;dr seems to be that some mathematicians think Jacob Lurie's work on infinity categories points to a better concept of equivalence than normal equivalence relations. Those mathematicians have been playing fast and loose with developing this theory, and now a few of them are trying to construct infinity categories of infinity categories that they think might fill holes in some of the less than rigorous work that's been going on. That sounds interesting, but unless higher category theory has any meaningful applications to non-mathematicians learning math in high school or undergraduate, saying that any of this will replace the equals sign or the standard notion of equivalence relations is overselling it.

Koshkin 5y ago
This page lists some applications outside mathematics: https://ncatlab.org/nlab/show/applications+of+%28higher%29+category+theory https://ncatlab.org/nlab/show/applications+of+%28higher%29+c...
stepchowfun 5y ago
> That sounds interesting, but unless higher category theory has any meaningful applications to non-mathematicians learning math in high school or undergraduate, saying that any of this will replace the equals sign or the standard notion of equivalence relations is overselling it. It's possible that our new understanding of equality as it appears in higher category theory and homotopy type theory will finally make working with proof assistants sufficiently practical for mathematicians, since it enables reasoning in a way that is closer to how mathematicians reason informally (treating isomorphic objects as equal, working with quotients, etc.). This area of research is obviously an active construction site, but we've seen incredible progress in the past two decades (e.g., cubical type theory). In high school, we often work informally with notions that have a more formal treatment as one progresses to university and graduate school. For example, in high school, one might be introduced to calculus by learning some rules for calculating derivatives and antiderivatives. Later, in university, those calculations are justified by real analysis. One could imagine a similar treatment of equality: in high school, we learn how to do equational reasoning by substitution, and then in university maybe we'd learn about (for example) how equality is defined as an inductive family and how substitution is justified by its corresponding induction principle. So, your comment seems a bit short-sighted or closed-minded to me, even if you're correct that this will not have any impact on high school mathematics. I just think that's a poor measuring stick for impact.
zozbot234 5y ago
This is conflating analytical descriptions of these potential mathematical objects for synthetic ones. Analytical characterizations ("how does this object arise") is what's sought in this kind of research, but a synthetic one ("here's a mini-language that formally describes this mathematical object, and the exactly-stated 'rules of the game' that ensure that you're using it correctly in a logical sense") is all that a high school student needs. High school students don't typically concern themselves with constructing, e.g. the real numbers as formal mathematical objects, but they need to know how to make correct statements in the language of real numbers. Note that synthetic descriptions are not "informal" in any sense; they're just as watertight logically as analytical ones, they just arrive at the result in a different, and arguably complementary way.

Koshkin 5y ago

This page lists some applications outside mathematics: https://ncatlab.org/nlab/show/applications+of+%28higher%29+category+theory https://ncatlab.org/nlab/show/applications+of+%28higher%29+c...

stepchowfun 5y ago

> That sounds interesting, but unless higher category theory has any meaningful applications to non-mathematicians learning math in high school or undergraduate, saying that any of this will replace the equals sign or the standard notion of equivalence relations is overselling it. It's possible that our new understanding of equality as it appears in higher category theory and homotopy type theory will finally make working with proof assistants sufficiently practical for mathematicians, since it enables reasoning in a way that is closer to how mathematicians reason informally (treating isomorphic objects as equal, working with quotients, etc.). This area of research is obviously an active construction site, but we've seen incredible progress in the past two decades (e.g., cubical type theory). In high school, we often work informally with notions that have a more formal treatment as one progresses to university and graduate school. For example, in high school, one might be introduced to calculus by learning some rules for calculating derivatives and antiderivatives. Later, in university, those calculations are justified by real analysis. One could imagine a similar treatment of equality: in high school, we learn how to do equational reasoning by substitution, and then in university maybe we'd learn about (for example) how equality is defined as an inductive family and how substitution is justified by its corresponding induction principle. So, your comment seems a bit short-sighted or closed-minded to me, even if you're correct that this will not have any impact on high school mathematics. I just think that's a poor measuring stick for impact.

zozbot234 5y ago

This is conflating analytical descriptions of these potential mathematical objects for synthetic ones. Analytical characterizations ("how does this object arise") is what's sought in this kind of research, but a synthetic one ("here's a mini-language that formally describes this mathematical object, and the exactly-stated 'rules of the game' that ensure that you're using it correctly in a logical sense") is all that a high school student needs. High school students don't typically concern themselves with constructing, e.g. the real numbers as formal mathematical objects, but they need to know how to make correct statements in the language of real numbers. Note that synthetic descriptions are not "informal" in any sense; they're just as watertight logically as analytical ones, they just arrive at the result in a different, and arguably complementary way.