No, sorry, but you haven't got the point of HoTT. $x \equiv y$ means "$x$ is the same as $y$", so they are terms such that one can be transformed into the other by "rewrite rules" such as expanding or invoking the meaning of a definition, changing the names of bound variables, $\beta$-reduction, etc. I suspect that you have a pure maths background rather than one in computer science (or category theory). In that case you should think of $Id(x,y)$, not as equality, but as the **fundamental group**. the space of **paths** from $x$ to $y$. When there is a path from $x$ to $y$, it does not mean that $x$ and $y$ are the same. Moreover, when $p$ and $q$ are paths from $x$ to $y$, $p$ and $q$ don't have to be the same, or even homotopic.