# Philipp Haselwarter: Extensional type theories for proof assistants

Date: 2. 10. 2017

Source: Mathematics and theoretical computing seminar

Source: Mathematics and theoretical computing seminar

Torek, 3. 10. 2017, od 12h do 14h, Plemljev seminar, Jadranska 19

**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.