In Martin-Löf type theory with identity eliminator

$$ J : \prod_{B:\prod_{x,y:A}(x=y)\to\mathcal{U}}\left( \prod_{x:A}B(x,x,\mathrm{refl}_x)\to \prod_{x,y:A}\prod_{p:x=y}B(x,y,p) \right) $$

satisfying $J(B,b,x,x,\mathrm{refl}_x)=b(x)$ we can have terms $p:x=x$ that are not equal to $\mathrm{refl}_x$.

We can then interpret the $x:A$ as points of a space, and the terms of $x=y$ as the paths joining $x$ and $y$. The loops $p:x=x$ that are not $\mathrm{refl}_x$ are interpreted as non-contractible loops. Terms of type $p=_{x=y}q$ are homotopies between paths, etc.

Now, I have seen that the univalence axiom is of great importance in homotopy type theory, but I don't see how it enters in this discussion. The question is: does univalence have consequences in the homotopy interpretation of type theory?

If the answer is yes, what role does it play?