Type theories and polynomial monads
De Steve Awodey
Apparaît également dans la collection : Categories in homotopy theory and rewriting / Catégories pour la théorie de l'homotopie et la réécriture
A system of dependent type theory T gives rise to a natural transformation p : Terms $\to$ Types of presheaves on the category Ctx of contexts, termed a "natural model of T". This map p in turn determines a polynomial endofunctor P : $\widehat{Ctx}$ $\to$ $\widehat{Ctx}$ on the category of all presheaves. It can be seen that P has the structure of a monad just if T has $\Sigma$-types and a terminal type, and that p is itself a P-algebra just if T has $\Pi$-types. I will explain this rather unexpected connection between type theories and polynomial monads, and will welcome any insights from the other participants regarding it.
![$k$-sum free sets in $[0,1]$](/media/cache/video_light/uploads/video/2015-09-10_de_Roton-video--19cf70874d3c5af7378c268cab865b06.jpg)
