Home > News > Guillaume Brunerie: A general class of dependent type theories

Guillaume Brunerie: A general class of dependent type theories

Date: 8. 3. 2020
Source: Mathematics and theoretical computing seminar
Četrtek, 12. 3. 2020, od 11h do 13h, učilnica 3.07, Jadranska 21
Abstract: In this talk I will present my take on defining a general class of dependent type theories (including Martin-Löf type theory and similar systems, but not modal/cubical type theories) for which one hopes to prove the initiality conjecture. This was developed independently from the similar work by Bauer-Haselwarter-Lumsdaine, but the result seems to end up being quite similar. If time permits, I will also discuss an ongoing formalisation of this definition in Agda.