The goal of the workshop is to bring together researchers to share recent
work on double categories and their applications to domains such as
computer science, type theory, applied category theory, and higher
category theory. The workshop will be open for everyone to attend online,
with recordings of the talks being uploaded after the workshop is finished.
Speakers have been invited to give talks all along the
“expository–technical” scale, so the workshop will hopefully be of interest
to both those who are new to double categories and want to learn about
the fundamental techniques and viewpoints, and also to domain
specialists who are interested in technical results and current topics of
active research.
We hope that this workshop will create a snapshot of the research area
as it currently stands together with directions for future work, as well as
provide an invitation to people wanting to know more about the area, or
who are wondering if the tools or ideas in double category theory might
be useful to their own research.
The 2022 workshop is now finished, but here you can find the abstracts, recordings, and slides of the talks given. We sincerely thank all speakers and participants for their contributions.
The title says it all. I will look at some examples as an excuse to introduce and motivate the basic concepts of double category theory. This way I hope to bring them to life so that, in the end, they might be considered as friends and not mere acquaintances (or worse). No prior knowledge of double categories will be assumed.
What do categories, preordered sets, metric spaces, and topological spaces have in common? They all have an underlying set, and, when viewed in the right way, they all have some additional data that relates the elements of the underlying set. For each of these kinds of mathematical objects, there are two natural kinds of morphisms. The usual kind of morphisms, which we will refer to merely as morphisms, consist of a function between the underlying sets, and a mapping of the additional data in the same direction as the function. For example, functors and continuous maps are morphisms of categories and topological spaces, respectively. The other kind of morphisms, which we will refer to as retromorphisms, consist of a function between the underlying sets, and a lifting of the additional data in the opposite direction to that of the function. For example, cofunctors and open maps are retromorphisms of categories and topological spaces, respectively. In all cases, the morphisms and retromorphisms assemble into a double category whose cells capture a notion of compatibility between the two kinds of morphisms.
Actually, for any double category with chosen companions, there is an associated double category of monad morphisms and monad retromorphisms, and all of the above examples arise in this way. My talk will give a gentle introduction to these double-categorical concepts, focusing on how the above examples and several more fit into the general theory. No prior knowledge about double categories will be assumed. This extends recent work (arXiv:2209.01144) on enriched cofunctors beyond the setting of enriched category theory.
An homotopical way to compare 2-categories and double categories
Paula Verdugo
Macquarie University
It has proven useful to study some aspects of 2-categories within the framework of double categories – for example, there are some 2-categorical universal properties that elude a purely 2-categorical description but show themselves naturally expressed in the double categorical world. In this talk we present ways to compare these two 2-dimensional worlds homotopically by means of model categories. If time permits, we will explore how we may generalize this idea to higher dimensions. This is joint work with Lyne Moser and Maru Sarazola. Basic knowledge about (2- and double) categories will be useful, together with the idea behind model categories.
Middle East Technical University, Northern Cyprus Campus
Formalising the classical notion of Yoneda embedding necessarily includes formalising the notion of "locally small functor", that is functors \(f\colon A\to C\) such that all homsets \(C(fa,c)\) are small. A Yoneda structure on a 2-category for instance includes the notion of "admissible morphism" which formalises that of locally small functor.
In a (generalised) double categorical approach to formal Yoneda embeddings, instead of postulating a notion of "locally small morphism", it is natural to regard all horizontal (say) morphisms to be "locally small". This gives an intrisic notion of local smallness which fruitfully interacts with other formal notions such as that of adjunct vertical morphism, fully faithful vertical morphism and restriction of horizontal morphisms.
The aim of this talk is to introduce a double categorical approach to formal Yoneda embeddings without presuming familiarity with formal category theory. Motivated by obtaining a common formalisation of the classical notions of generic subobject (of topos theory) and Yoneda embedding, we are led to consider "augmented virtual double categories" as the right setting for doing so. These generalise double categories by allowing cells with paths of horizontal morphisms as horizontal source and, as horizontal target, either a single horizontal morphism or an empty path. We conclude by looking at several formal results that involve formal notions of smallness such as, for instance, a description of the sense in which a formal presheaf object \(P\), defined by a formal Yoneda embedding \(y\colon A\to P\), is cocomplete.
National Technical University of Athens, School of Applied Mathematics and Physical Sciences
In this talk, we will describe how to formally extend the so-called arithmetic product of symmetric sequences to colored symmetric sequences, namely their many-object analogue. This requires general results on extending monoidal structures to Kleisli constructions, specifically in the world of double categories. Some basic knowledge of fibrant double categories is assumed, but involved concepts and tools shall be in general described throughout the talk.
Gray-type monoidal product and Bifunctor Theorem for double categories
Mathematical Institute of Serbian Academy of Sciences and Arts
In the introductory part we will recall what double categories are and we will show some examples that illustrate why double categories present a more suitable framework to work in than bicategories. We proceed by describing the construction of a Gray type monoidal product for double categories for two versions of morphisms: strict and lax double functors. Along the way we characterize (lax double) quasi-functors(in analogy to "quasi-functors of two variables" for 2-categories of Gray). We introduce their 2-category \(q\text{-}\operatorname{Lax}_{hop}(\mathbb{A}\times\mathbb{B},\mathbb{C})\) and construct a 2-functor \(\mathcal{F}: q\text{-}\operatorname{Lax}_{hop}(\mathbb{A}\times\mathbb{B},\mathbb{C}) \to \operatorname{Lax}_{hop}(\mathbb{A}\times\mathbb{B},\mathbb{C})\) to the 2-category of lax double bifunctors. This is a double category version of the Bifunctor Theorem, recently proved for 2-categories. We will show when this 2-functor \(\mathcal{F}\) restricts to a 2-equivalence. For a consequence we derive 2-functors known as currying and uncurrying functors in Computer Science, in the context of double categories. We finish by showing the application of the 2-functor \(\mathcal{F}\) on 2-monads. Concretely: we obtain that \(\mathcal{F}\) is a generalization to non-trivial double categories of the classical Beck's result, that a distributive law between two monads makes it possible for them to compose. It turns out that a distributive law is a specification of a (lax double) quasi-functor to trivial double categories. No prior knowledge of double categories is necessary, but knowing 2-categories, their functors, transformations and modifications is helpful.
Double Presheaf Categories via Polynomial Functors
The category Poly of polynomial functors on sets and natural transformations between them forms a monoidal category under composition. By results of Ahman–Uustalu and Garner, the bicategory of comonoids and bicomodules in Poly has as objects small categories and as morphisms from C to D familial (aka parametric right adjoint) functors from C-Set to D-Set, the categories of Set-valued functors from C and D. Familial functors between (co)presheaf categories are defined as disjoint unions of representables on each component, and include the free category monad on graphs and data migration functors between categories of databases.
Polynomial functors on categories also have a monoidal structure by composition, where the comonoids are precisely small double categories satisfying a factorization condition that includes most double categories in common use. Bicomodules between such double categories \(\bf C\) and \(\bf D\) induce "familial" double functors from \({\bf C}^t\)-Set to \({\bf D}^t\)-Set, the copresheaf double categories of lax double functors from the transpose of \(\bf C\) and \(\bf D\) to the double category of sets, functions, spans, and maps of spans.
I will introduce polynomial functors, comonoids and bicomodules, familial functors, and double copresheaf categories to build up to this result (joint with David Spivak) and its early implications for double category theory and categorical databases, assuming background only in double categories and ordinary (co)presheaf categories.
The free cornering of a monoidal category is a single-object double category obtained by adding companion and conjoint structure to it. If the morphisms of the monoidal category admit interpretation as processes, then this interpretation extends to the cells of the free cornering, which then admit interpretation as interacting processes. In this talk I will introduce the free cornering construction, explain its interactive interpretation, and survey a number of results surrounding the free cornering from both published and ongoing work.
Single-object double categories are much simpler than their more general counterparts. I expect that most of the talk will be accessible to anyone with even a surface understanding of monoidal categories, and in particular their string diagrams.
A double-categorical look at different flavours of factorisation system
Orthogonal factorisation systems are a simple and natural categorical structure that is not hard to grasp. Algebraic weak factorisation systems, which generalise the orthogonal ones, are not so straightforward, involving monads and comonads and quite a lot of structure to keep track of. However these structures can be approached via double categories and this double-categorical perspective is very useful. I will tell a bit of the story of the double-categorical approach to these structures.
Reporting on recent results of joint work with R. Harmer, P.-A. Melliès and N. Zeilberger, I will present a novel formalization of compositional rewriting theory via double categories. For a given rewriting theory, individual rewriting steps are formalized as 2-cells of a double category. One of the crucial aspects of compositionally consists then in providing a set of axioms that the double category of the rewriting system must satisfy in order to ensure the existence of concurrency and associativity theorems., which are quintessential for developing important applications of rewriting systems such as In combinatorics and Markov chain theory. Another concept central to this end, I.e., “counting modulo universal properties”, may be implemented via a certain presheaf and coend calculus. Time permitting, I will sketch how the counting calculus then leads to a categorification of the concept of rule algebras (which capture the combinatorics of interactions of rewriting steps).
In this talk, we consider approaches to exponentiability in double categories. For a 1-category \(\mathcal D\), one can define cartesian closure via a pointwise or a 2-variable adjunction, and arrive at equivalent definitions. The pointwise approach requires the existence of an exponential object \(Z^Y\), for every object \(Y\) of \(\mathcal D\), whereas for the latter, the exponentials are given by a bifunctor \({\mathcal D}^{\rm op}\times {\mathcal D}\to \mathcal D\). We will see that these two approaches differ for a double categories \(\mathbb D\). In particular, a bifunctor \({\mathbb D}^{\rm op}\times {\mathbb D}\to {\mathbb D}\) would involve not only objects of \(\mathbb D_0\), but also those of \(\mathbb D_1\), i.e., vertical morphisms of \(\mathbb D\).
We will assume some familiarity with double categories, but recall the definitions and properties of adjoints on double categories, as well as the relevant examples.
Universal properties play an important role in mathematics, as they allow us to make many constructions such as (co)limits, Kan extensions, adjunctions, etc. In particular, a universal property is often formulated by requiring that a certain presheaf is representable. The representation theorem gives a useful characterization of these representable presheaves in terms of initial objects in their category of elements. Going one dimension up and considering 2-categories, with tslil clingman we showed that the same results is true for Cat-valued presheaves if one considers their "double category of elements". In this talk, I will explain how to generalize the representation theorem to the more general framework of V-enriched categories, where V is a cartesian closed category. This is joint work with Maru Sarazola, and Paula Verdugo. Only basic knowledge of ordinary category theory will be assumed.
Segal-type models of weak 2-categories are simplicial models of bicategories, and they comprise the Tamsamani model and the more recent weakly globular double categories, introduced by Paoli and Pronk. Fair 2-categories, introduced by J. Kock, model weak 2-categories with strictly associative compositions and weak unit laws. This model has some features in common with the Segal-type models, but with the simplicial delta replaced by the fat delta, which encodes weak units.
I will illustrate a direct comparison of fair 2-categories with weakly globular double categories: this result sheds new light on the notion of weak globularity as encoding weak units and has potential for higher dimensional generalizations.
Framed bicategories are double categories having all companions and conjoints. Many structures naturally organize into framed bicategories, e.g. open Petri nets, polynomials functors, polynomial comonoids, structured cospans, etc. Symmetric monoidal structures on framed bicategories descend to symmetric monoidal structures on bicategories. The axioms defining symmetric monoidal double categories are more tractible, and arguably more natural, than those defining symmetric monoidal bicategories. It is thus convenient to study ways of lifting a given bicategory into a framed bicategory along an appropriate category of vertical morphisms. Solutions to the problem of lifting bicategories to double categories have been useful in expressing Kelly and Street's mates correspondence and in proving the higher dimensional Seifert-van Kampen theorem of Brown et. al., amongst many other applications. We consider lifting problems in their full generality.
Globularly generated double categories are minimal solutions to lifting problems of bicategories into double categories along given categories of vertical arrows. Globularly generated double categories form a coreflective sub-2-category of general double categories. This, together with an analysis of the internal structure of globularly generated double categories yields a numerical invariant on general double categories. We call this number the vertical length. The vertical length of a double category C measures the complexity of compositions of globular and horizontal identity squares of C and thus provides a measure of complexity for lifting problems on the horizontal bicategory of C. I will explain recent results on the theory of globularly generated double categories and the vertical length invariant. Minimal knowledge of double categories and bicategories will be assumed.
Fibrations and doubly lax colimits of double categories
Dalhousie University, Department of Mathematics and Statistics
Classically, the Grothendieck construction, or the category of elements, of a pseudo functor \(F\colon {\mathbf D}\to{\bf Cat}\) (also called the indexing functor) has two properties that define it (up to equivalence):
(A) it is the object part of the adjoint equivalence between the category of such pseudo functors, also called indexing functors, and the category of fibrations over \({\mathbf D}\);
(B) it is the lax colimit for the diagram defined by \(F\).
These two results have been shown to hold for suitably defined Grothendieck constructions for bicategories and \(\infty\)-categories and has been conjectured for weak \(n\)-categories. So when one is interested in colimits of double categories or fibrations between double categories we want to look for a suitable Grothendieck construction.
When we replace the category \({\mathbf D}\) above by a double category \({\mathbb D}\), the first question is what the codomain of the indexing functor should be. The issue is that \({\bf DblCat}\), the category of double categories, is not a double category. However, it is enriched over double categories: it has two classes of transformations (which I will call inner and outer) as local arrows and modifications as local double cells. In this talk I will present two replacements for \({\bf DblCat}\) in the definition of indexing functor. I will replace it with the quintet double category of the 2-category of double categories with double functors and outer transformations and I will replace it by the double 2-category \({\mathbb S}\mathrm{pan(Cat)}\) (and we will work with all lax functors). The first case has the advantage that the objects are still double categories. The second case is inspired by the fact that a lax double functor from the terminal double category into \({\mathbb S}\mathrm{pan(Cat)}\) corresponds to a double category.
The last type of indexing functor has an associated Grothendieck construction that can be viewed as a Grothendieck construction that is done in two layers and leads to a category object in a suitable category of fibrations: a double fibration. The first type of indexing functor leads us to a new notion of what we call a doubly lax transformation between double functors of the form \({\mathbb A}\to{\mathbb Q}{\mathcal D}_{\mathrm{outer}}\) where \({\mathcal D}\) is a \({\bf DblCat}\)-enriched category. These give then rise to a notion of doubly lax colimit for diagrams of double categories. These doubly lax colimits can be constructed using the double Grothendieck construction I will introduce, and have a universal property that is expressed in terms of both classes of 2-cells of \({\bf DblCat}\). Furthermore, it also has a canonical projection double functor to \({\mathbb D}\), the indexing double category, and this has the properties of a double fibration in one direction and a weaker fibration property in the other direction.
We will discuss how both constructions generalize various colimit and fibration constructions for 2-categories and bicategories and finally, we will consider how the two are related. A partial answer to this last question is given by the construction of a lax double functor \({\mathbb Q}{\bf DblCat}_{\mathrm{outer}}\to {\mathbb S}\mathrm{pan(Cat)}\).
This talk is based on work done with Geoff Cruttwell, Michael Lambert and Martin Szyld in [1] and work done with Marzieh Bayeh and Martin Szyld in [2].
Background needed for this talk: mainly, the basics of double categories - double functors, and horizontal and vertical transformations (here referred to as outer and inner transformations); familiarity with the Grothendieck construction and its properties is also useful.
[1] G.S.H. Cruttwell, M.J. Lambert, D.A. Pronk, M. Szyld, Double Fibrations, arXiv:2205.15240, and to appear in Theory and Applications of Categories (2022).
[2] Marzieh Bayeh, Dorette Pronk, Martin Szyld, The Grothendieck Construction for Double Categories, in progress.
Friday 2nd
Operads as double functors
Claudio Pisani
Independent researcher
The language of double categories provides a direct abstract approach to colored operads (that is, symmetric multicategories), enlightening and simplifying several classical facts and notions. Namely, an operad \(\mathcal{O}\), in its non-skeletal form, is a product-preserving lax double functor
\[
(\mathbb{P}\mathrm{b}{\mathbf{Set_f}})^{\mathrm{op}} \to \mathbb{S}\mathrm{et}
\tag{1}
\]
from the dual of the double category of pullback squares in finite sets to the double category of mappings and spans. This characterization can be rephrased in two ways. First, by a universal property of the monoid construction one can consider instead normal functors \((\mathbb{P}\mathrm{b}{\mathbf{Set_f}})^{\mathrm{op}} \to \mathbb{C}\mathrm{at}\). Second, by a double category of elements construction [1,2], operads are certain discrete double fibrations \(d:\mathbb{D} \to \mathbb{P}\mathrm{b}{\mathbf{Set_f}}\). The idea is that the proarrow part of \(\mathbb{D}\) is the category of families of objects and of arrows in \(\mathcal{O}\) (indexed by \({\mathbf{Set_f}}\)) and that families of arrows in \(\mathcal{O}\) can be reindexed along pullback squares in \({\mathbf{Set_f}}\).
Sequential operads [3], symmetric monoidal categories and commutative monoids are those operads \(\mathcal{O}\) for which the vertical part of \(d\) is a fibration, an opfibration or a discrete opfibration, respectively. In particular, we get the accompanying characterization of commutative monoids as product-preserving functors \((\mathbb{P}\mathrm{b} {\mathbf{Set_f}})^{\mathrm{op}} \to \mathbb{S}\mathrm{q}{\mathbf{Set}}\).
This approach suggests a notion of generalized operad obtained by replacing in (1) the category of finite sets with any category \(\mathcal{C}\). For instance, a category with small products (or sums) gives a generalized monoidal category with \(\mathcal{C} = {\mathbf{Set}}\), along with the corresponding generalized monoid of isomorphism classes. Furthermore, one can define cartesian operads in this more general setting and prove therein the equivalence between tensor products, universal products and algebraic products (as in the well-known case of categories enriched in commutative monoids).
We assume a basic knowledge of the language of double categories and of fibrations; some acquaintance with operads or multicategories would be helpful, even if the basic ideas will be recalled.
[1] M. Lambert, Discrete double fibrations, TAC37 (2021).
[2] R. Paré, Yoneda theory for double categories, TAC17 (2011).
[3] C. Pisani, Sequential multicategories, TAC29 (2014).
[4] C. Pisani, Fibered multicategory theory, arXiv (2022).
[5] C. Pisani, Operads as double functors, arXiv (2022).
From categorical systems theory to categorical cybernetics
Myers' categorical system theory is a double categorical yoga for describing the compositional structure of open dynamical systems. It unifies and builds on previous work on operadic notions of system theory, and provides a strong conceptual scaffolding for behavioral system theory. However, some of the most interesting systems out have a richer compositional structure than that of dynamical systems. These are cybernetic systems, or in other words, interactive control systems. Notable and motivating examples are strategic games and machine learning models. In this talk I’m going to introduce the tools and language of categorical system theory and outline how categorical cybernetics theory might look like. At the end, we will briefly venture into the triple dimension.
Center for Topological and Quantum Systems, NYU Abu Dhabi
(Joint with Matteo Capucci)
The Para construction takes a monoidal category \(M\) and gives a category \(\mathrm{Para}(M)\) where a morphism \(a \to b\) is a pair \((c, f : c \otimes a \to b)\) of a "parameter space" \(c\) and a parameterized map f in M. This construction formalizes the idea of separating inputs into special "control variables" or "parameters" which will be set separately from the other inputs to a process. The Para construction has played an important role in categorical accounts of deep learning — where it was first described by Fong, Spivak, and Tuyeras — open games, and cybernetics.
The Para construction has been generalized in a number of ways. First, it can take an action of a monoidal category \(M\) on a category \(C\) (an "actegory"). And second, the resulting category can be seen as the shadow of a bicategory where 2-cells are reparameterizations. In this talk, we will see a further generalization of the scope of the Para construction — we will take an actegory \(\otimes : M \times C \to C\) and produce a double category \(\mathbb{P}\mathrm{ara}(\otimes)\) whose vertical morphisms are parameterized by objects of \(M\) and whose horizontal morphisms are those of \(C\).
We will show that in this guise, the Para construction arises as a (pseudo)distributive law between the action double category of \(\otimes : M \times C \to C\) and the double category of arrows of \(C\), each seen as (pseudo)monads in a tricategory of spans in \(\mathsf{Cat}\). Our construction is abstract and applies in any suitably complete 2-category \(\mathbb{K}\), in particular in the 2-category of double categories with vertical transformations. This lets us construct a triple category \(\mathrm{Para}(\mathrm{Arena})\) whose morphisms are lenses, charts, and parameterized lenses respectively. The cubes in this triple category give representable behaviors of Capucci-Gavranovic-Hedges-Rischel cybernetic systems, and one of the resulting face double categories is a variant of Shapiro and Spivak's double category \(\mathbb{O}\mathrm{rg}\). The method of proof also suggests generalizing the domain of the Para construction to take any "dependent actegory", and at this level of generality the double category of spans in a cartesian category is revealed to be a sort of Para construction.
How can we tell whether a double category is a double category of relations on a regular category? Any such double category is at least an equipment and is cartesian, but what else is needed? This talk aims to present a characterization theorem that describes these further conditions. This result should be seen as a double-categorical version of the development due to Carboni and Walters that showed which bicategories occur as bicategories of relations on a regular category. This talk should be accessible to anyone who knows the basics of bicategories and double categories. Along the way, we will review the work of Carboni and Walters, and define what it means for a double category to be cartesian and to be an equipment. We will also talk about tabulators and in what way a double category can be seen as "functionally complete".
