2-Functoriality of Initial Semantics, and Applications
summary
Shows that initial semantics, when parametrized by the monoidal category of contexts, is 2-functorial: a monoidal functor or adjunction between base categories induces a functorial translation between the corresponding categories of models that preserves initial objects. Uses 2‑categorical machinery (monoidal categories, adjunctions/co‑reflections, curtain/sigma constructions) to lift relations like de Bruijn ↔ locally nameless and to equate implementations (e.g. FSSet vs Set^Set), yielding a co-reflection preserves initiality result and a generalized recursion principle for simply‑typed syntax.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 0:46Initial semantics recap
- 3:58Binders and reduction rules
- 5:22Modeling binders tradition
- 7:28Models over different categories
- 9:382-functoriality solution
- 11:062-categories in framework
- 12:09Untyped case and co-reflections
- 13:33Simply typed case and signatures
- 15:19Generalized recursion principle
- 17:47Summary: models are 2-functorial
- 18:54Questions and answers session
related talks
27mFunctorial Semantics for Partial Theories
21mFunctorial Syntax for All
02h 24mCategory Theory Track
23mFormalizing Monoidal Categories and Actions for Syntax with Binders
30mDisplayed Monoidal Categories for the Semantics of Linear Logic
46mProfunctor Optics: The Categorical Approach
23mFrom Semantics to Syntax: A Type Theory for Comprehension Categories
27mUnivalent Double Categories