Séminaire en ligne, 8 avril 2021
Pour assister à la rencontre, se rendre sur https://ent-services.ens-lyon.fr/entVisio/ choisir Chocola dans le menu déroulant, mettre son nom comme identifiant, et Bruxelles sans majuscule comme dernier champ. Autoriser les popups, et changer de navigateur au besoin.
10h: accueil et problèmes de connexion 10h15: début de l'exposé 11h15: questions et discussion 12h: adieu et problèmes de déconnexion Merci aux auditeurs de couper micro et caméra (sauf éventuellement, lorsqu'ils souhaitent poser une question). Les questions peuvent aussi être posées dans la fenêtre de chat.
En cas de problème ou de question, écrire à chocola-gestion chez ens-lyon.fr.
Programme
- 10:00 – 12:00
-
Daniel Gratzer (Aarhus University)Invited talk: Sketching type theories
Recent developments in type theory have attempted to systematically recast properties of the syntax of a type theories (canonicity, normalization, etc.) into equivalent questions about the category of models. This dictionary relies on a formal link between the syntax of a theory and its category of models: the syntax of the theory must organize into an initial model. To expedite this process, several logical frameworks have been proposed which provide schemata for defining a type theory so that it automatically determines a category of models in which syntax is initial.
In this talk, rather than giving a new logical framework per se, we propose a new discipline for creating logical frameworks based around finitary 2-monads and sketches. As a case study of this approach, we show how locally Cartesian closed categories provide a suitable doctrine for type theories. We illustrate how a general theory of sketches [KPT99] can be used to define syntactic categories for type theories in a style that resembles the use of Martin-Löf's Logical Framework [NPS90], following the "judgments as types" principle [HHP93, ML87].
We prove a semantic adequacy result for locally Cartesian closed categories relative to Uemura's representable map categories [Uem19]: if a theory is definable in the framework of Uemura, the locally Cartesian closed category that it generates is a conservative (fully faithful) extension of its syntactic representable map category. On this basis, we argue for the use of locally Cartesian closed categories as a simpler alternative to Uemura's representable map categories.
This is joint work with Jonathan Sterling, and a preprint is available on arxiv: https://arxiv.org/abs/2012.10783
