12
votes
3answers
442 views

Formal/rigorous treatment of (im)predicativity/predicativism

There are several places on the web where one may find quite intuitively understandable accounts of (im)predicativity; here on MO I found two questions with very good detailed answers (Predicative ...
5
votes
0answers
154 views

Feasible Type Theories

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 ...
4
votes
1answer
511 views

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