Roughly, the strong normalization property for Martin-Löf Intensional Type Theory (MITT) tells us that every closed term $t$ of type $M$ will eventually reach a canonical normal form $t’$ such that it a direct instance of the constructors of $M$.

Now let $A : Type$ with $a,b : A$. If my understanding is correct, for identity type, this means that all closed terms of some $a=b$, are of the form $refl ...$. I would like to better understand how such reduction happens in practice, so let me give you a toy example.

Consider $A, B : Type$ and $w : A \times B$. Thus, we have the type $$ w = (\text{pr1 } w, \text{pr2 } w) $$ and any closed term of it should be reducible to a normal form.

We want to construct explicitly such a closed term $t : w = (\text{pr1 } w, \text{pr2 } w)$, which we do by $$t := \text{prod_induction_principle } w \text{ } (λ a \text{ } b, (refl (a,b))) $$ But now how can we show that $t$ reduces to some term of the form $refl …$ ?

  • 4
    $\begingroup$ $t$ is not a closed term unless you are using $w$ as a meta-variable. $\endgroup$ – Derek Elkins left SE Apr 18 '16 at 3:04
  • 2
    $\begingroup$ Once you tell us what $w$ is we will be able to reduce $t$, yes. Until then it's a secret. $\endgroup$ – Andrej Bauer Apr 18 '16 at 5:58
  • $\begingroup$ @DerekElkins Thanks! This strictly speaking, also applies to $A,a, b$. However, in any case, it seems you can replicate the question by letting $t (A a b w)$ be the wanted closed term. $\endgroup$ – StudentType Apr 18 '16 at 5:58
  • 2
    $\begingroup$ Also, this is not a research-level question. It is more suitable for math.stackexchange.com or cs.stackexchange.com. $\endgroup$ – Andrej Bauer Apr 18 '16 at 5:59