m

F Nous contacter

0

Documents  Awodey, Steve | enregistrements trouvés : 2

O
     

-A +A

P Q

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

Research talks;Algebra;Logic and Foundations;Topology

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

... Lire [+]

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

- 256 p.
ISBN 978-0-19-856861-2

Oxford logic guides , 0049

Localisation : Ouvrage RDC (AWOD)

catégorie # logique # dualité # foncteur # catégorie de diagramme

18-01 ; 03-01 ; 03G30 ; 18A25

... Lire [+]

Z