Steve Awodey: Type theories and polynomial monads​

Abstract: A system of dependent type theory T gives rise to a natural transformation p : Terms → 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 : Ctxˆ → Ctxˆ on the category of all presheaves. It can be seen that P has the structure of a monad just if T has Σ-types and a terminal type, and that p is itself a P-algebra just if T has Π-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.

Recording during the thematic meeting "Categories in Homotopy Theory and Rewriting" the September 28, 2017 at the Centre International de Rencontres Mathématiques (Marseille, France)

Filmmaker: Guillaume Hennenfent

Find this video and other talks given by worldwide mathematicians on CIRM's Audiovisual Mathematics Library: http://library.cirm-math.fr. And discover all its functionalities:
- Chapter markers and keywords to watch the parts of your choice in the video
- Videos enriched with abstracts, bibliographies, Mathematics Subject Classification
- Multi-criteria search by author, title, tags, mathematical area

Видео Steve Awodey: Type theories and polynomial monads​ канала Centre International de Rencontres Mathématiques