Philipp Haselwarter: Extensional type theories for proof assistants

Abstract: We present Martin-Löf's type theory with equality reflection and discuss some of the difficulties that arise when we want to implement it in a proof assistant. We then present equivalent formulations of type theory that have better meta-theoretical behaviour and thereby attempt to remedy some of these problems.

This is joint work with Andrej Bauer, and work in progress.