# intensional equality in type theory

I want to know why we add an intensional equality in type theory to definitional equality ? What is the aim with this intensional equality ?

thanks

-
Intensional equality is decidable but extensional equality is not. I guess mathematics is not intensional since I can't decide whether or not that was the reason... –  François G. Dorais Aug 3 '12 at 1:32
Not all type theories use intentional equality. For example, Martin-Lof has developed type theories with intentional and with extensional equality. Each one has its own cons and pros. –  Kaveh Aug 3 '12 at 5:20
Do you mean to ask about intensional versus extensional equality, or propositional versus definitional/judgmental equality? Propositional equality can be either intensional or extensional (e.g. depending on whether or not it satisfies axiom K). –  Mike Shulman Aug 3 '12 at 5:28
Try looking at Chapter 8 of B. Nordström, et al., Programming in Martin-Löf’s Type Theory, intuitionistic.files.wordpress.com/2010/07/… –  Carl Mummert Sep 3 '12 at 11:33

## 1 Answer

The key thing to notice is that the definitional equality is a judgement and not a proposition (so in particular, definitional equalities can not be part of your assumptions, nor can they be proved, they can only be checked by the type-checker). The intensional equality, on the other hand, is a proposition, so it can be used as an assumption, and we can e.g. use induction to prove an intensional equality.

The two equalities are closely connected, but do not generally agree: Martin-Löf's intensional type theory has decidable type checking, and hence also the definitional equality judgement is decidable, but you can convince yourself that the intensional equality is not decidable.

Note that definitional equality entails intensional equality, but not the other way around.

-
As a clarification, the first paragraph here would also apply to an extensional, propositional equality. –  Mike Shulman Sep 3 '12 at 5:51
I believe kow is saying that one can use structural induction to prove an intensional equality, because there are rules to allow this, but there are not rules to manipulate definitional equality. –  Carl Mummert Sep 3 '12 at 11:29
thanks Kow it's clear now. –  Asymptotik Sep 16 '12 at 18:27