Algebraic structures from dependent type theory

Thursday, March 1, 2018 - 12:00
427 Thackeray Hall
Speaker Information
Clive Newstead
Carnegie Mellon University

Abstract or Additional Information

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.