# Understanding Strong Normalization for Identity Types in Martin-Löf Intensional Type Theory [closed]

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 …$ ?

• $t$ is not a closed term unless you are using $w$ as a meta-variable. – Derek Elkins left SE Apr 18 '16 at 3:04
• Once you tell us what $w$ is we will be able to reduce $t$, yes. Until then it's a secret. – Andrej Bauer Apr 18 '16 at 5:58
• @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. – StudentType Apr 18 '16 at 5:58
• Also, this is not a research-level question. It is more suitable for math.stackexchange.com or cs.stackexchange.com. – Andrej Bauer Apr 18 '16 at 5:59