> 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.
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.