I want to know why we add an intensional equality in type theory to definitional equality ? What is the aim with this intensional equality ?
MathOverflow is a question and answer site for professional mathematicians. It only takes a minute to sign up.Sign up to join this community
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.