I’m always amazed by how many subtle assumptions we often make when doing day-to-day maths, and how challenging these assumptions yield to some interesting construct.

I’m currently trying to read the Homotopy Type Theory (« Hott ») book. HoTT is an extension of type theory which is the underlying logic foundation of most proof assistant.
It uses the « proposition as type » idea which identifies some usual logical building block like conjunction, disjunctions, implications, quantifiers… with usual (and sometimes less usual) programming type constructs like algebraic types, functions…

One of the most important logical building block covered by type theory is the equality. To be honest I never really thought what « being equals to » really mean before reading the book, besides the usual « it’s just another equivalence relation between things ». But that’s neither a definition nor a satisfying properly, as for instance you can name several other equivalence like isomorphism which wouldn’t act as a good replacement for equality in most context.

Type theory gives two answers to this question : the first one is the definitional equality, or equality by definition. This equality comes from the fact that some composite type can be « reduced » : breaking a tuple into its component, or applying an argument to a function yield simpler syntaxical construct ; for instance in this framework (\x -> x + x)(1) (applying « 1 » to the lambda function which transforms « x » to « x + x ») is definitionally equals to 2, or fst (x, y) is definitionally equals to x. It’s just a matter of « following your nose » and determining if 2 objects are definitionally equal should better be decidable.
Unfortunatly not every equality is decidable in the day to day maths world : equality for reals is not decidable, there is no magic method to determine if 2 sides of an equation are equals. This means we need another kind of equality and here lie the second answer provided by type theory.
Type theory introduce an identity type, sometimes called « judgemental equality ». It’s a proposition and not merely a syntaxical rewriting. However the computation and uniqueness principle are designed to capture the defining property of equality which was hinted by the definitional equality : If two objects x and y are equals, then you can replace x by y in any proposition containing y (it’s a bit more involving but it’s the overall idea). Note that identity type is a generalisation of the definitional equality : an introduction rule for the identity type is equality by reflexivity, ie an object x is equals to itself. Since two definitionnaly equals objects are really just the same object in this framework, 2 definitionnally equals object are also judgmentally equals. But what are the others way to introduce equality then ?

That’s where Homotopy type theory comes into play. There are several answer to this question : one is that reflexivity is always the only way to introduce equality, and thus if 2 objects are equals one can consider that they are really the same. This is the logic under the Extensional Type Theory. There are several consequence to this design choice that I won’t cover.
On the other hand, homotopy type theory allows other kinds of « equalities » with root in homotopy (a subfield of topology as far as I understand which studies continuous path, path between path, and so on). It gives rise to a whole new interpretation of equality that is at the hearth of the book : objects are not merely « element in a set » but become « points in a space » whose path between point are equality relation.

I will write more on it later.