Håkon Robbestad Gylterud: Comonads of diagrams for dependent type theories

This talk presents the first part of an ongoing study of the syntax and semantics of dependent type theories as combinatorial objects. The first part investigates how systems of dependent sorts can be described using co-algebras of finite, wellfounded graphs. These co-algebras are compared to the notion of simple categories (also known as signatures of Makkai's First-Order Logic with Dependent Sorts). We will discuss how this approach can be extended to include terms of dependent sorts.