8 ms·

This discussion goes way beyond an "absolute layman explanation to homotopy type theory" ... Anyway, I disagree that the "whole idea of type theory is that th

This discussion goes way beyond an "absolute layman explanation to homotopy type theory" ... Anyway, I disagree that the "whole idea of type theory is that things can have more than one proof". UIP is about identity types and their proofs. Identity types are very special types. It is far from obvious that they should be inhabited by more than one proof. Indeed, it was a surprising breakthrough when Streicher/Hoffmann discovered that UIP does not hold in general and new axioms like Streicher's K or Univalence needed to be formulated to deal with this question.

jules 11y ago
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.

jules 11y ago

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.