In Homotopy Type Theory, do $x, y$ exist such that $x = y$ is inhabited but $x \not\equiv y$? I'm new to Homotopy Type Theory and am trying to understand the difference between judgemental and propositional equality.
To my understanding, if $x,y: A$ for any type $A$ and $x \equiv y$, then one may substitute the identity type $x =_A y$ for $x =_A x$ in any derivation. In other words, $x =_A y$ and $x =_A x$ are the same type. And since the latter is inhabited by refl$_x$, we have that $x$ and $y$ are propositionally equal.
My question is, how does this work the other way around? If the identity type $x =_A y$ is inhabited, does judgemental equality ($x \equiv y$) follow?
If so, is judgemental equality just there to give different names to types?
 A: In Homotopy Type Theory, such a type, an x and a y certainly can and do exist.
First, a basic example. Define $m * n$ on natural numbers by recursion on $n$. Thus, in particular, $2 * n$ is $2 + ... + 2$ rather than $n + n$. Then if $n$ is a natural number in the context, then $n + n$ and $2 * n$ are propositionally equal (provable by induction), but not definitionally equal. The issue is this $n$ that's in the context. If we knew what $n$ was, we'd be able to evaluate $2 * n$ and $n + n$ to see that they're the same number. As it is, we can't.
To avoid this issue of things in the context, we might ask for closed terms - ones with an empty context (no free variables). If we turn $2 * n$ and $n + n$ into functions of $n$, then we get closed terms and functional extensionality tells us they these functions are propositonally equal. But because $2 * n$ isn't convertible into $n + n$ (with the usual rules), $\lambda n. 2 * n$ and $\lambda n. n + n$ are also not definitionally equal.
With univalence, we can give more examples. $\mathbb{N} + 1 = \mathbb{N}$ because the two types are equivalent, and by univalence that means they're propositionally equal. They are not definitionally the same, though.
Further examples are furnished by higher inductive types. For example, the interval $I$ has two basic points and an equality between them. While this type is equivalent to a singleton type, the two points are not definitionally equal.

Outside of HoTT (but still within type theory), it's consistent to posit exactly what you propose: that propositional equality implies definitional equality. This is called the equality reflection rule. One consequence of this addition is that all types become 0-types (sets) in the sense of HoTT. Another consequence is that type checking becomes undecidable. To check if a term has a given type, you might have to prove propositional equalities, which can be arbitrarily hard.
