|
In some sense, basically every field of math makes this kind of distinction. e.g. it's acknowledged that for a vector space V, the tensor products V⊗(V⊗V) and (V⊗V)⊗V are not equal, but they are equivalent in the sense of e.g. a linear isomorphism, or maybe in the sense of an algebra isomorphism or something, and mathematicians do have machinery to track in what sense they consider two non-equal things to be equivalent, and they take the time to prove that operations they want to define on equivalent but non-equal things give equivalent results. Category theory is partly concerned with this kind of machinery. So they do care about this, but then invented ideas like equivalence relations and quotients so that they can not have to constantly care about it. With programming languages or a proof assistant like lean, by default non-equal things are not the same, and you need to do some bookkeeping to carry around proofs that things are equivalent in the way you need them to be. The tricky thing is actually making it ergonomic to be able to think of (1+1)+1 and 1+(1+1) as "the same" without constantly needing to think about it. It's hard to do math in most programming languages partly because they lack the machinery necessary to have contextual notions of equivalence (but also because they lack dependent types). In some fields, that extra bookkeeping is really important. E.g. in geometry you might be able to choose coordinate systems at each point of some space, but perhaps not in a way that is globally defined and consistent with the types of equivalence that you need, so you need to track everything through local coordinate changes as you move around. Or a simpler example is a vector space and its dual: they're isomorphic, so in some sense equivalent, but not canonically so, so you need to track the equivalence you're using, and maps on one are "mirrored" when applied to the other. More generally, any finite dimensional vector space is characterized (in the sense of equivalence up to linear isomorphism) by a single number (its dimension), so in some sense it "is" that number, but we also think of them as each being different, depending on context. So f.d. vector spaces can in some sense be thought of as "numbers that remember which vector space they are". |