What is a canonical term of $\text{Id}_A(x,y)$ if $x$ is not jugdmentally identical to $y$?

Question

In the context of constructive type theory, a term inhabiting some type is said to be in canonical form if it is explicitly built up using the constructors of that type.

Particularly, the only constructor of the identity type of $A$ is $\text{refl }: \Pi x. \text{id}_A \text{ } x \text{ } x$, so

Question 1: What is a canonical term of $\text{Id}_A(x,y)$ if $x$ is not jugdmentally identical to $y$?

Apparently there cannot be such a canonical term, for neither $\text{refl } x$ nor $\text{refl } y$ type check. Does this mean that the identity type of $A$ does not have a canonical form in general? That is, that $\text{Id}_A(x,y)$ only has a canonical form in the particular case where $x$ is judgmentally equal to $y$?

But in this case how propositional equality differs in practice from judgmental equality then – except for the fact that the former occurs as a type and the other as a judgment?

Question 2: What is a closed term of $\text{Id}_A(x,y)$? Are there two closed terms $p, q$ of $\text{Id}_A(x,y)$ such that $p$ and $q$ are not judgmental equal?

Answer 1

1. Yes, in general $\mathrm{Id}_{A}(x, y)$ will not have a canonical form. Consider the case when $x$ and $y$ are distinct free variables -- obviously you can postulate that $x$ and $y$ are equal, but you can't provide a proof of it.

   Even more simply, consider the empty type $0$. It has no canonical forms at all, but there's nothing stopping you from assuming that a variable has type $0$.

2. For standard type theory, it is provably the case that if you have a closed term $t$ of type $\mathrm{Id}_{A}(x, y)$, then $x$ and $y$ are definitionally equal.

   Since the language is normalizing and $t$ is well-typed in the empty context, then we know that $t$ will evaluate to $\mathrm{refl}(z)$ for some $z$, and then by inversion we will be able to establish that $z \equiv x \equiv y$ judgementally.