# 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