I am looking for references about efficient type theories, efficiency in the sense of computational complexity, and type theory in the sense of Martin-Lof's type theories. Has there been any studies ...
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