# Tagged Questions

**12**

votes

**3**answers

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

**0**answers

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

**1**answer

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