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.
Certainly there are types systems that have rules of the kind that you propose, but the idea of HoTT is quite different from those. The clue is in the name: homotopy type theory (or indeed homotopy type theory).
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.
Even when $p$ and $q$ are homotopic, so there is some $u:Id(p,q)$, there may be another $v:Id(p,q)$ that is not the same as (or homotopic to) $u$. And so on.