Peter LeFanu Lumsdaine: Martin Hofmann’s conservativity theorems
Tid: On 2015-05-06 kl 10.00 - 11.45
Plats: Room 16, building 5, Kräftriket, Department of mathematics, Stockholm university
Two notable conservativity results in dependent type theory are due to Martin Hofmann: the conservativity of the logical framework presentation of a type theory, and the conservativity of extensional type theory over intensional type theory with extensionality axioms.
I will discuss these two theorems, and the general status of conservativity results in dependent type theory.
This will be an entirely expository talk.