A seminar talk presented at the Programming Languages Seminar.

Abstract

In joint work with Niels van der Weide, we have developed a framework for constructing ``univalent models’’ of type theories, in homotopy type theory. In this seminar slot, I provide some motivation for this work.