Definition of "set" in HoTT

Question

In the homotopy type theory book (https://hott.github.io/book/nightly/hott-online-1007-ga1d0d9d.pdf) "set" is defined as follows (see chapter 3):

Definition 3.1.1. A type A is a set if for all x, y : A and all p, q : x = y, we have p = q.

Can you explain this definition to a layman? What is the intuition behind it? Is this a definite describtion of what a set is?

Answer 1

Because "the equality for type A" is itself a type, we are naturally led to consider "the equality for type (the equality for type A)" and "the equality for type (the equality for type (the equality for type A))", etc., etc. There is a whole tower of such types.

Types for which this tower of "the equality for type (...)" gets boring at some point are interesting in their own right. Depending where that level is, you get different names. For instance:

• propositions are "boring" types: all their elements are equal. The intuition behind this name is that we only care about whether a proposition is provable or not, we do not care about the proofs themselves (so it's fine to consider them all to be equal).

• sets are types for which the equality type is itself a proposition: you can have different elements but, between two such elements, all the equality proofs are equal.

A few examples:

• The empty type is a proposition: all its elements are equal

• The datatype Bool is a set: there is not structure hiding in the proof that true = true or false = false.

• The type of sets is something else: Bool for instance can be equal to itself in two different fashions (The identity and negation functions are two distinct isomorphisms between Bool and Bool, giving rise to two distinct equality proofs).

Answer 2

In homotopy type theory , types behave like spaces (up to homotopy), and x=y is like the space of paths from x to y. Homotopically, therefore, this definition says that, if x and y are connected by a path, then there is only one such path up to homotopy. Thus, each connected component of A is contractible (has no nontrivial loops or higher loops), so up to homotopy A is determined by a set, namely its set of connected components. Inside HoTT we can't tell the difference between a contractible space and a point, so we may as well say that A is a set.