Instances of models of double-categorical theories
Kevin Carlson, Evan Patterson
TL;DR
The paper develops a unified notion of instance for models of cartesian double theories, extending the classical idea of presheaves and profunctors to the double-category setting. It shows that such instances are equivalently described by discrete opfibrations over the model, and it builds a comprehensive factorization framework in which these fibrations form the right class. The results extend to cartesian double theories, where cartesian instances correspond to cartesian discrete opfibrations, and lead to algebraic (finite-product) presentations and multicategory interpretations. The work further explores multicategorical examples, cocartesian/symmetric variants, and a modal double-theory extension, highlighting applications to algebraic profunctors and categorical databases and suggesting future directions in modal theory and presentability. Collectively, the framework provides a robust, algebraic approach to instances, fibrations, and factorization in double-categorical settings with practical implications for database theory and higher-morder morphisms.
Abstract
We contribute a chapter in common to categorical database theory and to the study of higher morphisms between double categories. The common thread here is the notion of instance, or right module, which we generalize from functors from a plain category into Set to the models of a (cartesian) double theory. This provides a concept of instance for such objects as a category equipped with a monad, or a (symmetric) multicategory, recovering the multifunctors into Set in the latter case. We also show that instances of models are equivalent to an appropriate concept of discrete opfibration over that model, not recoverable as the representable discrete opfibrations in the 2-category of models. Finally, we give comprehensive factorization systems with these discrete opfibrations as the right class.