Understanding the issue of equality in Homotopy Type Theory (HoTT) is easier if you are a programmer

We programmers know something that mathematicians don't really appreciate: equality is a tricky concept. Lets illustrate this with a straightforward example in some generic OO programming language. I am trying to make this language-independent and neither use any exotic concepts nor ban any common ones, but use whatever makes the issue easy to illustrate. 

interface Real;

interface Complex: getReal(); getImg(); getAbs(); getArg(); ... 

class Cartesian implements Complex: 

    Real x, y 

    Cartesian(x', y'): x = x'; y = y'

    getReal(): x

    getImg(): y

    getAbs(): sqrt(x*x + y*y) 

    getArg(): arctan(x/y)

    ...

 

class Polar implements Complex: 

    Real r, t    

    Polar(r', t'): r = r'; t = t' 

    getReal(): r * cos t

    getImg(): r * sin t

    getAbs(): r

    getArg(): t

    ...

We have the well trodden example of complex numbers with two implementations, Cartesian and Polar. 

Now, how can two Complex numbers c1 and c2 be equal?

Most superficially, if the language allows reference testing c1 and c2 are equal if they are the same reference, i.e. the same memory location, i.e. the "same thing" in an almost physical way. If not, they are in some sense "not equal" as there is an operation distinguishing them, namely reference-equality testing. But this is pretty much the only operation that can distinguish them, and a pretty particular one. This is not usually what we want. 

A deeper comparison is to compare the data, but that can only happen if the two Complex numbers are both Cartesian or both Polar. In this case, if their x, y members (or, respectively r, t, members) are equal then the two Complex numbers are also equal. 

If the type of Reals is a built-in type, for example that of floating point numbers, then they have a standard notion of equality, so we are done. But what if the type of Reals is itself an interface? There are, for example, several ways in which arbitrary precision Reals can be implemented in order to avoid the rounding errors that are so difficult to manage in the case of floating point. 

To compare Reals as an abstract data types (interface) we are back to the same situation: compare them as references (not good) or compare whatever data members they have, if they belong to the same class instantiating the interface. 

So the issue of equality is pretty complicated to begin with. But what about comparing Complex numbers from different classes? What about the Cartesian with x=y=0 and the Polar with r=t=0? They both represent the same (abstract) Complex number, i.e. the same point in the Complex plane, no matter what system of coordinates we use, Cartesian or Polar -- namely 0. The fact that x=y=r=t=0 is a coincidence, as the same could be said about points x=0, y=1 vs r=1, t=pi/2 which both represent the complex number i, or any complex number and its two implementations. 

This forces us to ask a deeper question: the two representations of Complex numbers 0 or i are clearly not "equal" if we peek under the covers. They rely on different implementations. However, if we have no access to the implementation, we can be sure that any program written just with Complex numbers and their interface will be unable to differentiate between them. We simply cannot write a function that returns a different result, when given either of the implementations of the same complex numbers, either Cartesian or Polar. This makes the two implementation of the same complex number intersubstitutable, hence equal. Note that certain low-level primitives in real-life languages (e.g. hash functions) could still distinguish them and break the equality. 

Mathematicians do not have to struggle, usually, with the issue of multiple implementations of the same concepts. This is why they tend to be happy enough with the notion of equality that says that two things are equal if their representations are equal. This is how equality is managed in the most common foundation of mathematics, set theory. However, some mathematicians such as Grothendieck, noticed that sometimes this is not good enough. These slides [PDF] are a very accessible introduction to the problem. (And in fact they were the motivation of this blog post.)

HoTT is a newer foundation of mathematics, much less settled than set theory, which takes a more refined view of equality. This makes it in some sense more complicated at the outset, when the objects are simple, but there is an expectation that this higher initial investment is worth it in the long term as we need to handle more complex mathematical objects. I am not going to say more about HoTT here, but hopefully you will have now understood why equality is such a sophisticated concept in it, unlike in good old fashioned set theory. 

Especially if you are a programmer, you will hopefully relate.