Functorial Semantics for Partial Theories
summary
Provides a Lawvere-style syntax for theories with partially defined operations by replacing cartesian string diagrams with string diagrams for partial maps built from copying, restriction and sameness operators, and specified generators and equations. Models are symmetric monoidal functors into Par and model morphisms are lax natural transformations. Works through examples (separation algebras, categories, partial combinatory algebras, cartesian closed examples) and proves a variety theorem: the categories obtainable this way are exactly the categories of models = locally finitely presentable categories and free models exist.
AI-written summary · about
chapters (16)
- 0:00Intro
- 0:48Overview
- 2:14Algebraic Theories
- 3:15Categories of Terms
- 6:19Finite Products
- 6:49Models
- 7:33Modelmorphisms
- 9:18Commutative command
- 9:54String diagrams
- 11:14Partial algebraic theories
- 13:33Sameness
- 15:39Partial Algebraic Theory
- 17:38Separation Algebras
- 20:11Modelmorphism
- 21:13Categories
- 25:20Variety Theorem
related talks
26m2-Functoriality of Initial Semantics, and Applications
21mFunctorial Syntax for All
02h 24mCategory Theory Track
45mA categorical view of computational effects
30mDisplayed Monoidal Categories for the Semantics of Linear Logic
51mA Gentle Introduction to Modern Model Theory
23mFrom Semantics to Syntax: A Type Theory for Comprehension Categories
24mTowards a Higher-Order Mathematical Operational Semantics