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
1

Type theories and polynomial monads

Sélection Signaler une erreur
Multi angle
Auteurs : Awodey, Steve (Auteur de la conférence)
CIRM (Editeur )

Loading the player...

Résumé : 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.

Codes MSC :
03B15 - Higher-order logic and type-theory
03F35 - Second- and higher-order arithmetic and fragments
03G30 - Categorical logic, topoi
55Pxx - Homotopy theory
55U40 - Topological categories, foundations of homotopy theory

    Informations sur la Vidéo

    Réalisateur : Hennenfent, Guillaume
    Langue : Anglais
    Date de Publication : 28/09/2017
    Date de Captation : 28/09/2017
    Collection : Exposés de recherche
    Sous Collection : Research talks
    Catégorie arXiv : Logic ; Category Theory
    Domaine(s) : Logique et Fondements ; Algèbre ; Topologie
    Format : MP4 (.mp4) - HD
    Durée : 00:56:01
    Audience : Chercheurs
    Download : https://videos.cirm-math.fr/2017-09-28_Awodey.mp4

Informations sur la Rencontre

Nom de la Rencontre : Categories in homotopy theory and rewriting / Catégories pour la théorie de l'homotopie et la réécriture
Organisateurs de la Rencontre : Ara, Dimitri ; Fiore, Marcelo ; Guiraud, Yves ; Mimram, Samuel
Dates : 25/09/2017 - 29/09/2017
Année de la rencontre : 2017
URL de la Rencontre : http://conferences.cirm-math.fr/1773.html

Données de citation

DOI : 10.24350/CIRM.V.19225103
Citer cette vidéo: Awodey, Steve (2017). Type theories and polynomial monads. CIRM. Audiovisual resource. doi:10.24350/CIRM.V.19225103
URI : http://dx.doi.org/10.24350/CIRM.V.19225103

Voir Aussi

Bibliographie



Sélection Signaler une erreur