m
• E

F Nous contacter

0

# Documents  Awodey, Steve | enregistrements trouvés : 2

O

P Q

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

## Type theories and polynomial monads Awodey, Steve | CIRM H

Multi angle

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 ...

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

## Category theory Awodey, Steve | Clarendon Press 2006

Ouvrage

- 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

#### Filtrer

##### Codes MSC

Titres de périodiques et e-books électroniques (Depuis le CIRM)

Ressources Electroniques

Books & Print journals

Recherche avancée

0
Z