 Voevodsky 2015 introduced the following stratification of types. (This stratification was motivated in part by this interpretation of a type as a topological space, but can be understood directly without reference to this interpretation.) We say that a type \(A\) is a proposition if we have \(\mathbf{Id}_A (a,b)\) for any element \(a\) and \(b\) of \(A\) (this means that the type \(A\) has at most one element). We say that a type \(A\) is a set if the type \(\mathbf{Id}_A (a,b)\) is a proposition for any element \(a\) and \(b\) of \(A\). We say that a type \(A\) is a groupoid if the type \(\mathbf{Id}_A (a,b)\) is a set for any element \(a\) and \(b\) of \(A\). The justification of this terminology is that it can be shown, only using the rules of type theory, that any such type can indeed be seen as a groupoid in the usual categorical sense, where the objects are the elements of this type, the set of morphisms between \(a\) and \(b\) being represented by the set \(\mathbf{Id}_A (a,b)\). The composition is the proof of transitivity of equality, and the identity morphism is the proof of reflexivity of equality. The fact that each morphism has an inverse corresponds to the fact that identity is a symmetric relation. This stratification can then be extended and we can define when a type is a 2-groupoid, 3-groupoid and so on. In this view, type theory appears as a vast generalization of set theory, since a set is a particular kind of type. 