Déposez votre fichier ici pour le déplacer vers cet enregistrement.

Multi angle  Type theories and polynomial monads
Awodey, Steve (Auteur de la Conférence) | CIRM (Editeur )

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

Filtrer

Domaine
Codes MSC
Audience

Z
ng'>
G

F Nous contacter


0

Documents  03F35 | enregistrements trouvés : 1

O
     

-A +A

P Q