It's true that it was a discovery that Martin Lof identity types could have multiple inhabitants, but it's a general principle of type theory that types can hav

It's true that it was a discovery that Martin Lof identity types could have multiple inhabitants, but it's a general principle of type theory that types can have multiple inhabitants (unlike in set theory, where propositions are just true). That this also applies to identity types in HoTT is a sign that something is going right. Furthermore, from another perspective it's "obvious" that identity types should have multiple inhabitants. There were two approaches to equality in type theory. One is Martin Lof identity types, which follow naturally from Leibniz' principle that A and B are equal then they are indistinguishable. The other is defining equality for each type on a case by case basis (pairs are equal if their components are equal, functions are equal if they give equal outputs, etc.), like in section 2.4 Equality of this paper: http://www.andres-loeh.de/PiSigma/PiSigma.pdf http://www.andres-loeh.de/PiSigma/PiSigma.pdf In the latter approach it's obvious that equality has multiple inhabitants, because it's defined that way. For example we can define equality of unordered pairs as the type: id_unordered_pair : (A,A) -> (A,A) -> Type id_unordered_pair (a,b) (c,d) = (id_A a c)*(id_A b d) + (id_A a d)*(id_A b c) i.e. two unordered pairs (a,b) and (c,d) are equal if a=c and b=d or a=d and b=c. This has two inhabitants even if id_A has only a single inhabitant. This approach naturally accommodates quotient types. The problem with it is that the type system has no idea that this is equality. It's just another definition. The point of equality is that all functions respect equality (equal inputs to equal outputs). Not all functions respect equality on these unordered pairs (e.g. a function that extracts the first component). This approach to equality has the converse of Leibniz' rule: we can define equality so that if two things are indistinguishable then they are equal. I think a good view of HoTT is as unifying these two approaches to equality. We get both Leibniz' principle and its converse, and we get user defined equality types whose equality is respected by all functions, we get multiple inhabitants for equality types.