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

Bookmarks Report an error
Multi angle
Authors : Awodey, Steve (Author of the conference)
CIRM (Publisher )

Loading the player...

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

MSC Codes :
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

    Information on the Video

    Film maker : Hennenfent, Guillaume
    Language : English
    Available date : 28/09/2017
    Conference Date : 28/09/2017
    Subseries : Research talks
    arXiv category : Logic ; Category Theory
    Mathematical Area(s) : Logic and Foundations ; Algebra ; Topology
    Format : MP4 (.mp4) - HD
    Video Time : 00:56:01
    Targeted Audience : Researchers
    Download : https://videos.cirm-math.fr/2017-09-28_Awodey.mp4

Information on the Event

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

Citation Data

DOI : 10.24350/CIRM.V.19225103
Cite this video as: 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

See Also

Bibliography



Bookmarks Report an error