Difference between Propositional and Judgmental Equality I'm reading the  HoTT  book and actually I'm a bit confused on core difference between
propositional equality (noation: $a=_A b$ where $a, b:A$ and judgmental equality
$ a \equiv b $.
The propositional equality is just a proposition and therefore a type $a=_A b$ and
checking if $a=_A b$ is true is equivalent to find a term $t: a=_A b$.
In contrast $ a \equiv b $ is a judgement, so statement about the theory and
not in. In the book one involved reason why we need also the judgmental equality
is to be able to make reasonable definitions like declaring a function
$f: A \to B$ to be $x^2$: $f(x) \equiv x^2$.
Intuitively this differs from propositional equality because it's a definition
we did and the theory not 'knows it'. So it seems senseless to try to prove
in the theory if $f(x) = x^2$, because we defined it so while the theory
we want to talk about is stiff, informally speaking 'we cannot define something
within the theory'.
At least, that's how I understood the difference between propositional equality
and judgmental equality. First of all, is this 'intuition' correct or
'misleading' and(or) wrong? The reason why I think that it might be shortcoming is the remark
on page 19 that 'As type theory becomes more complicated, judgmental equality
can get more subtle than this.' So I doubt that what I write above hits
to essential nature of the difference between propositional
and judgmental equality.
Question: Can the difference between propositional and judgmental equality made
be precise and does it coinside with my understandings of it sketched above
or did I miss the point?
 A: Your intuition is correct, but is a simplified understanding of the difference between propositional and judgemental equality. That's exactly the meaning of the sentence in the HoTT book that you are quoting in chapter 1.1: this chapter is meant to be an introduction to help understand type theory, and does not pretend to be exact and exhaustive in the details.
When you try to formalize a (informal) theory, you end up with a syntaxical representation of the objects of the theory, and syntaxic rules to manipulate these objects. With a simple theory, each object has a unique syntaxical representation: then there is no need of definitional (or judgmental) equality.
But most of the time, it is impossible to have a single syntaxical representation of each object; then you need to add additional rules, the conversion rules, that specify when 2 different syntaxical expressions represent the same object in the theory. 2 syntaxical expressions are definitionaly equal when they are different representations of the same object in the theory.
For instance, you usually want to ignore the differences in the naming of the variables: you need an $\alpha$-conversion rule to specify that two expressions differing only by the names encode the same object of theory.
Then you have the computation rules, that identify the syntaxical representation $f(a)$ with the result of the computation of $f$ applied to $a$ ($\beta$-conversion). You also want to identify an expression using notations with the expression obtained by replacing the notation by its definition.
The exact border between definitional and propositional equality is not always easy to draw (e.g. this note). It may be desirable, e.g. to simplify the formal proofs, that two objects that are proved to be propositionally equal are made definitionally equal with a new specific conversion rule. This can possibly be done with an equality reflection rule; however, such a rule has an impact on the meta-theoretical properties of the theory, such as the decidability of type checking.
It is desirable that, in the formalization of a theory, objects have a unique syntaxical representation, or, at least, can be converted into a unique syntaxical representation (strong normalization property). For a theory dealing with simple objects, propositional equality is then trivial and reduces to definitional equality. But for a theory dealing with more complex objects such as spaces or structures, admitting possibly different equivalent definitions inside the theory, the desired notion of equality of objects (space or structure) should be an equivalence of objects (space or structure), and therefore cannot be reduced to the definitional equality. Homotopy type theory and its univalence axiom is meant to achieve such a goal.
