Domov > Obvestila > Guillaume Brunerie: A general class of dependent type theories

Guillaume Brunerie: A general class of dependent type theories

Datum objave: 8. 3. 2020
Vir: Seminar za temelje matematike in teoretično računalništvo
Č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.