<ol>
<li><p>Yes, in general <span class="math-container">$\mathrm{Id}_{A}(x, y)$</span> will not have a canonical form. Consider the case when <span class="math-container">$x$</span> and <span class="math-container">$y$</span> are distinct free variables -- obviously you can postulate that <span class="math-container">$x$</span> and <span class="math-container">$y$</span> are equal, but you can't provide a proof of it.</p>
<p>Even more simply, consider the empty type <span class="math-container">$0$</span>. It has no canonical forms at all, but there's nothing stopping you from assuming that a variable has type <span class="math-container">$0$</span>.</p>
</li>
<li><p>For standard type theory, it is provably the case that if you have a closed term <span class="math-container">$t$</span> of type <span class="math-container">$\mathrm{Id}_{A}(x, y)$</span>, then <span class="math-container">$x$</span> and <span class="math-container">$y$</span> are definitionally equal.</p>
<p>Since the language is normalizing and <span class="math-container">$t$</span> is well-typed in the empty context, then we know that <span class="math-container">$t$</span> will evaluate to <span class="math-container">$\mathrm{refl}(z)$</span> for some <span class="math-container">$z$</span>, and then by inversion we will be able to establish that  <span class="math-container">$z \equiv x \equiv y$</span> judgementally.</p>
</li>
</ol>

CC BY-SA 3.0
2016-04-27T07:16:53.130Z
Let me put on my provably crusade hat: "provably the case" as opposed to "unprovably the case"?
Andrej Bauer
CC BY-SA 3.0
2016-04-27T07:18:07.870Z
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).
Andrej Bauer
CC BY-SA 3.0
2016-04-27T08:44:18.663Z
@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.)
Neel Krishnaswami
CC BY-SA 3.0
2016-04-27T09:31:12.737Z
Type theory is never as strong as my meta-logic. That would make my meta-logic too weak to study type theory.
Andrej Bauer
CC BY-SA 3.0
2016-04-25T13:22:55.913Z
2016-04-27T08:44:37.447Z
2020-06-17T09:38:08.363Z
Neel Krishnaswami
<p>In the context of constructive type theory, a term inhabiting some type is said to be in <em>canonical form</em> if it is explicitly built up using the constructors of that type. </p>

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

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

<p>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$ <strong>does not have a canonical form in general</strong>? That is, that $\text{Id}_A(x,y)$ only has a canonical form in the particular case where $x$ is judgmentally equal to $y$?</p>

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

<blockquote>
  <p><strong>Question 2:</strong> 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?</p>
</blockquote>

<type-theory><dependent-type><typed-lambda-calculus>
What is a canonical term of $\text{Id}_A(x,y)$ if $x$ is not jugdmentally identical to $y$?
StudentType
# What is a canonical term of $\text{Id}_A(x,y)$ if $x$ is not jugdmentally identical to $y$?

(Asked by: username_0 on 2016-04-25)

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?

**Tags:** type-theory, dependent-type, typed-lambda-calculus


---

## 1 answers

### Answer by username_1 on 2016-04-25. Score: 6

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.

> **Comments:**
> **username_2**: Let me put on my provably crusade hat: "provably the case" as opposed to "unprovably the case"?  
> **username_2**: 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).  
> **username_1**: @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.)  
> **username_2**: Type theory is never as strong as my meta-logic. That would make my meta-logic too weak to study type theory.  

---

