Models of type theory in univalent Type Theory
The master thesis On Initial Categories with Families by Konstantinos Brilakis, http://publications.lib.chalmers.se/records/fulltext/255039/255039.pdf, is a study of models of type theory in Agda.
The goal of this project will be to reformulate some results and represent them in univalent Type Theory using the fact that function extensionality is provable and if possible, making use of univalence, to formulate initiality results in a nice way.
Prerequisites: Familiarity with Agda and type theory or having taken the course DAT350/DIT233 Types for programs and proofs.The project is suitable for 1 or 2 students.
Contact: Thierry Coquand firstname.lastname@example.org