Guillaume Brunerie: A general class of dependent type theories

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.