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.

The expression $x\equiv y$ is not a type and does not have an extension.

The type $x=y$, written $Id(x,y)$, is that of the paths between $x$ and $y$, or of the proofs that $x$ and $y$ are equivalent, or of the equivalences between $x$ and $y$.