En poursuivant votre navigation sur ce site, vous acceptez l'utilisation d'un simple cookie d'identification. Aucune autre exploitation n'est faite de ce cookie. OK

Documents 03G30 1 results

Filter
Select: All / None
Q
Déposez votre fichier ici pour le déplacer vers cet enregistrement.
y

Type theories and polynomial monads - Awodey, Steve (Author of the conference) | CIRM H

Multi angle

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.[-]
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 ...[+]

03B15 ; 03G30 ; 03F35 ; 55Pxx ; 55U40

Bookmarks Report an error