2024 | 2022

The goal of the workshop is to bring together researchers, with a focus on those early in their career, 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.

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 also 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 2024 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.

Bryce and Tim

Monday 21st	Thursday 24th	Tuesday 29th	Wednesday 30th
Miloslav Štěpán	Nima Rasekh	Maru Sarazola	Dylan McDermott
Adrian Miranda	Jaco Ruit	Evan Patterson	Rui Prezado
	Lander Hermans	Keisuke Hoshino

Monday 21st

Double categories versus factorization systems

Miloslav Štěpán

Masaryk University

In the first part of the talk we will recall double categories and show that every orthogonal factorization system can be turned into a double category, every (nice) double category can be turned into an orthogonal factorization system, and that these processes are mutually inverse. We will do the same thing for strict factorization systems.

In the second part of the talk we will put the above results into a wider perspective of 2-category theory: if the double category is regarded as a diagram in Cat, producing the factorization system out of it amounts to taking a certain 2-categorial colimit of it (the codescent object). We will mention the connections to lax morphisms of algebras for a 2-monad, compositions of pinwheels, and possible extensions of the first part to weak factorization systems.
The pseudomonad perspective on double categories, with applications to double profunctors

Adrian Miranda

University of Manchester

Just as a category is a monad in the bicategory Span(Set), so a double category is a pseudomonad in the analogous tricategory Span(Cat). Pseudo-bimodules of between these give a notion of double profunctor, and these in turn specialise to recover double functors. Composition of double profunctors uses a two-dimensional colimit which, unlike the reflexive coequalisers of the standard internal category setting, are stable under pullback in Cat. We extend Grandis and Pare’s strictification results for double categories and double functors to analogous strictification results for double profunctors. We recover the tricategory PsDblCat whose morphisms are double functors, and describe work in progress, joint with Nicola Gambino, towards a tricategory PsDblProf whose morphisms are double profunctors. Finally, a dual specialisation of double profunctors will also be described giving a notion of double cofunctor, establishing the tricategory that these maps form, and providing a strictification result for them.

Thursday 24th

Double Categories in Univalent Foundations

Nima Rasekh

Universität Greifswald

This is joint work with Niels van der Weide, Benedikt Ahrens and Paige Randall North. In category theory, we typically study categories either up to isomorphisms (considering objects up to equality) or equivalences (considering objects up to isomorphism). Fortunately, since equivalences generalize isomorphisms, this distinction rarely causes mathematical difficulties. However, double categories present a richer structure with multiple notions of equivalence—such as isomorphisms, horizontal equivalences, and gregarious equivalences—none of which subsumes all the others. This creates potential ambiguities, making it necessary to specify the appropriate form of equivalence in any given context. In this talk, I will show how moving from a set-theoretic foundation to a univalent foundation allows for definitions of (double) categories that inherently include the desired notion of equivalence.
A double ∞-categorical approach to formal ∞-category theory

Jaco Ruit

Utrecht University

Formal ∞-category theory starts with the observation that there are many variants of ∞-category theory, for example, enriched ∞-categories, internal ∞-categories, and monoidal ∞-categories, which come with specialized notions of adjunctions, point-wise Kan extensions, and so on. It is natural to ask whether one can give a uniform and synthetic treatment of the foundational concepts and theorems for these different flavors of ∞-category theory. In this talk, we propose an extension of the ideas from formal (strict) category theory of Street-Walters, Wood, Verity, and Shulman, to the ∞-categorical context, and give a leisurely introduction to the theory of ∞-equipments. These ∞-equipments are certain double ∞-categories in which many concepts of category theory may be developed and expressed (using only the double categorical structure). We will present an overview and highlight some of these aspects. Now, since this approach yields category theories for the objects of these ∞-equipments, developing a category theory for a flavor of ∞-categories is a question of constructing the right suitable ambient ∞-equipment. Throughout the talk, we discuss some of these examples of ∞-equipments.
Virtual double categories as coloured box operads

Lander Hermans

University of Antwerp

Virtual double categories are a \(2\)-categorification of multicategories and compare to double categories as multicategories compare to monoidal categories. In algebraic topology, multicategories are also known as coloured operads and are extensively used to encode algebraic operations, thus generalizing operads.

In this talk we will generalize operads to box operads fitting the following scheme:

By viewing virtual double categories as coloured versions of box operads, we shift our point of view: from objects of study to algebraic gadgets encoding higher operations. This is exemplified by our main application: we present a box operad \(\mathrm{Lax}\) encoding lax functors \(\mathcal U \longrightarrow \mathrm{Cat}(k)\) into the category of \(k\)-linear categories. They appear in algebraic geometry as prestacks generalizing structure sheaves and (noncommutative) deformations thereof.

In the second part of the talk, I will sketch key components of our main result: a Koszul duality for box operads. For example, to every box operad we can associate a canonical \(\mathrm{L}_\infty\)-algebra. A salient feature is that these results can be explained purely in terms of (virtual) double categorical diagrams, or in our terms, stackings of boxes.

If time permits, I will explain how it applies to \(\mathrm{Lax}\) in order to tackle their deformation and homotopy theory.

Tuesday 29th

Double-categorical frameworks for algebraic K-theory

Maru Sarazola

University of Minnesota

In the last few years, double categories have made an appearance in the world of algebraic K-theory. The goal of this talk is to introduce the main ideas in some of these new K-theoretical frameworks, highlighting their different features and possible uses. No prior background on K-theory will be assumed.
Double-categorical logic in theory and practice

Evan Patterson

Topos Institute

Category theory contains a broad array of gadgets out of which to build specialized logics, as explored in categorical logic and programming language theory. Double category theory can organize and systematize the use of these categorical gadgets. In the first part of the talk, I review joint work with Michael Lambert on double theories and their models. Double theories are categorified theories whose models are categories equipped with extra structure. In the second part, I show how this work can be put to practical effect. I describe ongoing work with collaborators at Topos Institute to build CatColab, an interactive environment for formal, interoperable, conceptual modeling. In technical terms, CatColab is a structure editor for models of domain-specific logics, as defined by double theories.
Double categories of relations relative to factorisation systems

Keisuke Hoshino

Kyoto University

The double category of relations and the double category of spans have historically been key examples in the study of double categories. More generally, given a class \(\mathcal{M}\) of morphisms in a finitely complete category \(\mathbf{C}\), one can define an \(\mathcal{M}\)-relation \(A \nrightarrow B\) as a span that belongs to \(\mathcal{M}\) as a morphism into \(A\times B\). If \(\mathcal{M}\) is the right class of a stable factorisation system, the \(\mathcal{M}\)-relations and morphisms in \(\mathbf{C}\) form a double category.

In this talk, I will first give a characterisation of double categories that arise from stable factorisation systems in this manner.

I will then explore how different classes of stable factorisation systems can be characterised in terms of their corresponding double categories. This include the (regular epi, mono) factorisation system on a regular category, which has been studied by Carboni and Walters in terms of cartesian bicategories, and by Lambert in terms of cartesian double categories. By considering the (isomorphism, all) factorisation system, we also recover the double category of spans, a structure that has been examined bicategorically by Lack, Walters, and Wood, and double-categorically by Aleiferi. I will explain how these known results are related to our general theorem.

This talk is based on joint work with Hayato Nasu, and the results can be found in our paper available at arXiv:2310.19428.

Wednesday 30th

The formal theories of presheaves and cocompletions

Dylan McDermott

University of Oxford

Many categories can usefully be seen as completions of other categories under classes of colimits. For instance, if we freely add small colimits to a small category A then we get presheaves on A, and every finitely accessible category arises by completing a small category under filtered colimits. The theory of cocompletions of a V-category A is well-developed, at least for V a symmetric monoidal closed category, in particular, it is known that every such cocompletion is given by taking a class of presheaves on A. I will talk about some ongoing work to develop a formal categorical analogue of this theory, in a double-categorical setting. We obtain generalizations of some of the existing results: we can easily specialize our results to V-categories, even without assuming V is symmetric. But we also learn more about how cocompletions behave. The usual universal property of a cocompletion turns out to be too weak, so we find the appropriate generalization. The formal theories of presheaves and cocompletions also begin to diverge, exposing differences that are invisible in the enriched setting, though we find conditions that enable us to construct cocompletions from presheaves.

This talk is based on joint work with Nathanael Arkor (Tallinn University of Technology).
Change-of-base for generalized multicategories

Rui Prezado

Universidade de Aveiro
A multicategory is a categorical structure that consists of objects and multimorphisms, whose domain consists of a finite (possibly empty) string of objects, and whose codomain consists of a single object. Their composition and identity, as well as the unity and associativity properties, are well modeled by the extension of the free monoid monad on \(\mathsf{Set}\) to the (proarrow) equipment \(\mathsf{Span}(\mathsf{Set})\) of spans in \(\mathsf{Set}\). Multicategories, together with their respective functors, can be obtained by considering a suitable kind of algebra with respect to the extended free monoid monad on \(\mathsf{Span}(\mathsf{Set})\).

This abstraction can be carried out with any cartesian monad \(T\) on a category \(\mathcal A\) with pullbacks. We have an extension of \(T\) to the equipment \(\mathsf{Span}(\mathcal{A})\) of spans in \(\mathcal A\), and the respective "\(T\)-algebras" are the so-called \(T\)-categories internal to \(\mathcal A\), whose category we denote by \(\mathsf{Cat}(T,\mathcal A)\). Most importantly, if we are provided with another cartesian monad \(S\) on a category \(\mathcal B\), and a suitable monad morphism \((F,\phi) \colon (\mathcal A, T) \to (\mathcal B, S)\), it was shown in [3] that \((F,\phi)\) induces a change-of-base functor \(\mathsf{Cat}(T,\mathcal A) \to \mathsf{Cat}(S,\mathcal B)\).

The enriched counterpart of such generalized multicategories were first considered in [1]; in essence, enriched \((T,\mathcal V)\)-categories can be obtained as the "\(T\)-algebras" for a suitable monad \(T\) on the equipment \(\mathcal V\)-\(\mathsf{Mat}\), where the enriching category \(\mathcal V\) is a suitable monoidal category. Likewise, these also have a notion of change-of-base functors.

In general, we can consider horizontal lax \(T\)-algebras [2] for a lax monad \(T\) on a pseudodouble category \(\mathbb D\), special cases of which are enriched and internal generalized multicategories. This talk aims to present notions of change-of-base functors between such horizontal lax algebras, the study of which was motivated by understanding the relationship between enriched and internal multicategorical structures, the main topic of study of [4], joint work with F. Lucatelli Nunes.

We assume the basics of double category theory, and some familiarity with multicategories will prove to be worthwhile.
1. M. M. Clementino, W. Tholen. Metric, topology and multicategory -- a common approach. J. Pure Appl. Algebra, (179):13--47, 2003.
2. G. Cruttwell, M. Shulman. A unified framework for generalized multicategories. Theory Appl. Categ., 24(21):580--655, 2010.
3. T. Leinster. Higher Operads, Higher Categories, volume 298 of London Mathematical Society Lecture Note Series. Cambridge University Press, 2004.
4. R. Prezado, F. Lucatelli Nunes. Generalized multicategories: change-of-base, embedding and descent. To appear in Appl. Categ. Structures.

Second Virtual Workshop
on Double Categories

Selected days from 21st – 30th of October, 2024

2024 | 2022

Monday 21st

Double categories versus factorization systems

Miloslav Štěpán

Masaryk University

The pseudomonad perspective on double categories, with applications to double profunctors

Adrian Miranda

University of Manchester

Thursday 24th

Double Categories in Univalent Foundations

Nima Rasekh

Universität Greifswald

A double ∞-categorical approach to formal ∞-category theory

Jaco Ruit

Utrecht University

Virtual double categories as coloured box operads

Lander Hermans

University of Antwerp

Tuesday 29th

Double-categorical frameworks for algebraic K-theory

Maru Sarazola

University of Minnesota

Double-categorical logic in theory and practice

Evan Patterson

Topos Institute

Double categories of relations relative to factorisation systems

Keisuke Hoshino

Kyoto University

Wednesday 30th

The formal theories of presheaves and cocompletions

Dylan McDermott

University of Oxford

Change-of-base for generalized multicategories

Rui Prezado

Universidade de Aveiro

Second Virtual Workshopon Double Categories

Selected days from 21st – 30th of October, 2024

2024 | 2022

Monday 21st

Double categories versus factorization systems

Masaryk University

The pseudomonad perspective on double categories, with applications to double profunctors

University of Manchester

Thursday 24th

Double Categories in Univalent Foundations

Universität Greifswald

A double ∞-categorical approach to formal ∞-category theory

Utrecht University

Virtual double categories as coloured box operads

University of Antwerp

Tuesday 29th

Double-categorical frameworks for algebraic K-theory

University of Minnesota

Double-categorical logic in theory and practice

Topos Institute

Double categories of relations relative to factorisation systems

Kyoto University

Wednesday 30th

The formal theories of presheaves and cocompletions

University of Oxford

Change-of-base for generalized multicategories

Rui Prezado

Universidade de Aveiro

Second Virtual Workshop
on Double Categories