Peter LeFanu Lumsdaine: Martin Hofmann’s conservativity theorems
Time: Wed 2015-05-06 10.00 - 11.45
Location: 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.