Algebraic structures from dependent type theory

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.