How did Vladimir Voevodsky "changed the meaning of the equals sign"? This article from The New York Times is an obituary of the recently deceased Dr. Voevodsky. It explained that he was deeply involved in developing computer proof verification, and to do so "changed the meaning of the equal sign" and "reformulated mathematics from its very foundation". 
As the article is targeted to a general audience, it does not go into details. 
Can someone explain the meaning of these two quotes from the New York Times? 
(I believe they are related)
 A: The paradigm shift here — which didn't originate with Voevodsky — is that equivalence is generally a more important notion than equality. There is a quirk that makes achieving the shift difficult: equivalence is often more complex than simply a yes/no proposition.
For example, in group theory, it's much more important to talk about whether two groups are isomorphic than whether they are equal. In fact, it's rather uncommon to do the latter.
As an example of the added complexity, consider the first isomorphism theorem of groups. The main conclusion is often stated as

If $\varphi : G \to H$ is a group homomorphism, then $G/\ker(\varphi)$ is isomorphic to $\mathrm{im}(\varphi)$

but that's only part of what it says: the first isomorphism isn't merely saying "there is an isomorphism", but that the specific function $\overline{x} \mapsto \varphi(x)$ is said isomorphism.  (where $\overline{x}$ denotes the congruence class of $x$)
Talk of "changing the meaning of the equals sign" is, IMO, somewhat hyperbolic. Really, it's just describing the fact that if you have a way to reason and calculate in a way where equivalence really is the primary notion, it's useful to repurpose the symbol "=" to mean equivalence. (and if you really need the notion of equality, to find some other way to express it)

A great answer should mention homotopy type theory and/or the univalence axiom. It should also mutter something about the development of $\infty$-category theory and the search for internal languages, and also about the semantics of identity types in intensional type theory. I'm not ambitious enough to try and write a great answer, so I'll just mention the terms here to give hints for further reading.
