 Martin-Löf 1975 [1973] introduced a new basic type \(\mathbf{Id}_A (a,b)\), if \(a\) and \(b\) are in the type \(A\), which can be thought as the type of equality proofs of the element \(a\) and \(b\). An important feature of this new type is that it can be iterated, so that we can consider the type \(\mathbf{Id}_{\mathbf{Id}_A (a,b)}(p,q)\) if \(p\) and \(q\) are of type \(\mathbf{Id}_A (a,b)\). If we think of a type as a special kind of set, it is natural to conjecture that such a type of equality proofs is always inhabited for any two equality proofs \(p\) and \(q\). Indeed, intuitively, there seems to be at most an equality proof between two elements \(a\) and \(b\). Surprisingly, Hofmann and Streicher 1996 designed a model of dependent type theory where this is not valid, that is a model where they can be different proofs that two elements are equal. In this model, a type is interpreted by a groupoid and the type \(\mathbf{Id}_A (a,b)\) by the set of isomorphisms between \(a\) and \(b\), set which may have more than one element. The existence of this model has the consequence that it cannot be proved in general in type theory that an equality type has at most one element. This groupoid interpretation has been generalized in the following way, which gives an intuitive interpretation of the identity type. A type is interpreted by a topological space, up to homotopy, and a type \(\mathbf{Id}_A (a,b)\) is interpreted by the type of paths connecting \(a\) and \(b\). (See Awodey et al. 2013 and [HoTT 2013, Other Internet Resources].) 