Talk #1 title: Algebraic structures from dependent type theory
Abstract: There are many different notions of ‘model’ of dependent type theory, with each notion allowing us to view it in a different way. In recent work with Steve Awodey, we used the notion of a natural model to view dependent type theory through the lens of polynomial functors—this allowed us to identify a surprising monoid-like structure in the syntax of dependent type theory. This talk will be a high-level overview of our results and the ideas behind the proofs; I will assume basic knowledge of category theory but no knowledge of dependent type theory.
Talk #2 title: An infinite descent into pure mathematics
Abstract: A few years ago, I wrote a set of lecture notes for a course I was teaching over the summer. Various factors led to this evolving, almost by accident, into a fully fledged textbook. In this talk, I will discuss my experience of writing a textbook alongside doing my PhD research, with emphasis on the research-based pedagogical principles underlying its design.
Slides: available here.