Peter LeFanu Lumsdaine: Initiality for a general class of type theories
Tid: On 2018-10-10 kl 10.00 - 11.45
Plats: Room 16, building 5 kräftriket, Department of Mathematics, Stockholm University 
Medverkande: Peter LeFanu Lumsdaine (Stockholm University)
Abstract: I will present a definition of a general class of dependent type theories, and sketch a proof of an initiality result for such theories. I will give some comparison with Guillaume Brunerie’s independent work on the same topic, presented in the seminar last month. If time allows, I will also present an ongoing formalisation of this work. (This is joint work with Andrej Bauer and Philipp Haselwarter.)
This will to some extent recapitulate previous seminars I’ve given on this work, but will aim to be self-contained and comprehensive.