$isSet(A):={\large\Pi}_{x,y:A}\,isProp(Id_A(x,y))$

The sets as defined in HoTT are easier to understand when contrasted against more difficult structures. For example, if we consider two groups $G,G':groups$ which are isomorphic in five different ways (isomorphism will be defined as invertible group homomorphism in this case), then, due to the existence on an isomorphism they are the same for all practical purposes. All five isomorphisms demonstrate $G=_{group}G'$. Thinking in terms of set theoretic models of a group, an isomorphism might permute elements $x,y$ of $G$ while keeping $G$s group structure intact. Now if we consider two elements of a set $x,y:A$, then since being together in a set shouldn't constitute any structural relations, there are also no elaborate means of them being the same, unless the expressions $x$ and $y$ can be tracked back to come from the same definition, i.e. if they are definitionally the same. The definition above says that a type $A$ is a set if the identity on their elements doesn't derive from interesting isomorphisms but is just am matter of yes or no.

$isSet(A):={\large\Pi}_{x,y:A}{\large\Pi}_{p,q:Id_A(x,y)}\,Id_{Id_A(x,y)}(p,q)$

Identity type