00:00:00 / 00:00:00

Type theories and polynomial monads

By Steve Awodey

Appears in collections : Categories in homotopy theory and rewriting / Catégories pour la théorie de l'homotopie et la réécriture, Exposés de recherche

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.

Information about the video

Citation data

  • DOI 10.24350/CIRM.V.19225103
  • Cite this video Awodey, Steve (28/09/2017). Type theories and polynomial monads. CIRM. Audiovisual resource. DOI: 10.24350/CIRM.V.19225103
  • URL https://dx.doi.org/10.24350/CIRM.V.19225103

Last related questions on MathOverflow

You have to connect your Carmin.tv account with mathoverflow to add question

Ask a question on MathOverflow




Register

  • Bookmark videos
  • Add videos to see later &
    keep your browsing history
  • Comment with the scientific
    community
  • Get notification updates
    for your favorite subjects
Give feedback