I used to have the same annoyance about group and category theory; learning some about the type-theory-as-foundations work (particularly homotopy type theory an

I used to have the same annoyance about group and category theory; learning some about the type-theory-as-foundations work (particularly homotopy type theory and cubical type theory) has helped w/ this; in that setting, you have several distinct but well-developed notions of equality: propositional equality, which group theory and most math cares about, vs judgemental equality, which is the one that's "obviously true" by the rules of the system. e.g. 5 = 5 is true under judgemental and propositional equality, whereas x + 2 = 2 + x is only true under propositional