Some Remarks about Impredicativity - Thierry Coquand

Abstract: I will try to present the calculus that I designed in 1984–85, inspired by the works of de Bruijn, Girard and Martin-Löf, and what were the main problems at the time. I will compare it to the system of Frege, and explain how it provides a uniform notation for terms and proofs in higher-order logic (∀t : (t ⟶ ο) ⟶ ο with t ::= ι extended by not just t ::= ... | ο | ι → t but by t ::= ... | ο | t1 → t2) and proofs of parametricity. I will also explain how it was possible to represent inductive definitions. Next, I will connect it with the work about paradoxes in type theory and how this suggested the extension with universes. If time allows, I will explain what were the problems with an encoding of inductive data types, and why this was extended with primitive inductive definitions.