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?


1 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.

  • 1
    $\begingroup$ Let me put on my provably crusade hat: "provably the case" as opposed to "unprovably the case"? $\endgroup$ Apr 27, 2016 at 7:16
  • $\begingroup$ Also, the OP is usig the word "judgementally" so it may be better to use the same word instead of "definitionally" (which is not as good as "judgmentally" in my opinion). $\endgroup$ Apr 27, 2016 at 7:18
  • 1
    $\begingroup$ @AndrejBauer: The assumption that you can prove strong normalization means you are assuming that you have some kind of induction principle strong enough to prove it. But if the type theory is as strong as your metalogic, then it will indeed be unprovably the case that $x$ and $y$ are judgementally equal! (I like neither "judgementally" nor "definitionally", but have no superior alternative.) $\endgroup$ Apr 27, 2016 at 8:44
  • $\begingroup$ Type theory is never as strong as my meta-logic. That would make my meta-logic too weak to study type theory. $\endgroup$ Apr 27, 2016 at 9:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.