Double-categorical logic
in theory and practice

Second Virtual Workshop on Double Categories

Evan Patterson

Topos Institute

2024-10-29

Why double categories?

My personal favorite answers:

  1. Double categories unify functional and relational thinking
    • Understand relations, spans, profunctors, etc via universal properties
  2. Double categories are the setting for open systems:
    • An open system is both an object and a morphism
    • Hence is a proarrow in a double category
  3. Double category theory is an organizing framework for categorical logic

This talk is mostly about (3).

For (1), see blog post: Why double categories? Part 1

Categorical logic

Originates with Lawvere’s functorial semantics of algebraic theories:

Logic Category theory
algebraic theory category \(\mathsf{T}\) with finite products
model of theory functor \(M: \mathsf{T} \to \mathsf{Set}\) preserving finite products
model homomorphism natural transformation \(M \Rightarrow N\)

Lawvere (1963)

Categorical logic, the minimal setting

A minimalist account of relational databases:

Logic Category theory
schema small category \(\mathsf{C}\)
instance of schema functor \(X: \mathsf{C} \to \mathsf{Set}\)
morphism of instances natural transformation \(X \Rightarrow Y\)

Already enough to produce notable capabilities, such as Spivak’s functorial data migration.

Spivak (2012)

Standard dictionary of categorical logic

Logic Category theory
theory \(\mathsf{T}\) category \(\mathsf{T}\) with extra structure
model of \(\mathsf{T}\) in \(\mathsf{S}\) structure-preserving functor \(M: \mathsf{T} \to \mathsf{S}\)
model morphism structure-preserving natural transformation \(M \Rightarrow N\)


Categorical logic is two-dimensional:

  • Theories, models, and model morphisms form a 2-category
  • Such 2-categories are sometimes called “doctrines”
  • E.g., categories, monoidal categories, categories with finite products, … are objects of different doctrines

Another dictionary of categorical logic?

A sleight of hand in that story:

  • I replaced \(\mathsf{Set}\) with an arbitrary “semantics category” \(\mathsf{S}\)
  • That flexibility is useful, but \(\mathsf{Set}\) still plays a distinguished role


If we take this seriously, we might propose a different dictionary:

Logic Category theory
theory \(\mathsf{T}\) category \(\mathsf{T}\) with extra structure
model of \(\mathsf{T}\) structure-preserving module (copresheaf) over \(\mathsf{T}\)
model morphism structure-preserving module homomorphism

Categorical logics are double categories

Let us refine the dictionary of categorical logic:

  • interpretations of one theory in another are structure-preserving functors
  • models of a theory are structure-preserving modules (copresheaves)

But the latter are special kinds of bimodules or profunctors. So the two concepts are united within a double category!


Our starting point:

A categorical logic (doctrine) is a double category of categories equipped with extra structure.

This talk is about a systematic way to work with such categorical logics.

Outline

  • Part 1: Theory
    Double theories, a double-categorical framework for categorical logic
  • Interlude: Demo
  • Part 2: Practice
    CatColab, a collaborative environment for modeling in domain-specific categorical logics

Part 1: Double theories

Joint work with Michael Lambert.

Main references:

  1. “Cartesian double theories: A double-categorical framework for categorical logic” (Lambert and Patterson 2024)
  2. “Products in double categories, revisited,” Section 10: “Finite-product double theories” (Patterson 2024)

Toward two-dimensional functorial semantics

A lax functor

\[ F: \mathbb{1} \to \mathbb{S}\mathsf{pan}\]

is the same thing as a small category.

Moreover, a natural transformation is the same thing as a functor:

Second observation doesn’t work for lax functors between bicategories!

Toward two-dimensional functorial semantics

Generalizing from the terminal double category:

Proposition

Let \(\mathbb{D}\) be a strict double category and let \(F: \mathbb{D} \to \mathbb{S}\mathsf{pan}\) be a lax functor.

  • For each object \(x \in \mathbb{D}\), the data \((Fx, F\mathrm{id}_x, F_{x,x}, F_x)\) is a category

  • For each arrow \(f: x \to y\) in \(\mathbb{D}\), the data \((Ff, F\mathrm{id}_f)\) is a functor

  • For each special cell \(\alpha\) in \(\mathbb{D}\), the image \(F\alpha\) is a natural transformation:

Lambert and Patterson (2024), Section 2

Toward two-dimensional functorial semantics

Proposition

Let \(\mathbb{D}\) be a strict double category and let \(F: \mathbb{D} \to \mathbb{S}\mathsf{pan}\) be a lax functor.

  • For each proarrow \(m: x \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle+$}}\mkern-13mu{\to}}y\) in \(\mathbb{D}\), the data \((Fm, F_{x,m}, F_{m,y})\) is a bimodule, i.e., a profunctor

  • For each cell \(\alpha\) in \(\mathbb{D}\), the image \(F\alpha\) is a bimodule homomorphism, i.e., a natural transformation

These are the basic notions of category theory! Moreover, replacing \(\mathbb{S}\mathsf{pan}\) with:

  • \(\mathbb{S}\mathsf{pan}(\mathsf{C})\) gives notions internal to \(\mathsf{C}\)
  • \(\mathbb{M}\mathsf{at}(\mathcal{V})\) gives notions enriched in \(\mathcal{V}\)

Lambert and Patterson (2024), Section 2

Double theories

With this motivation, we propose that:

  • A “double theory” is a strict double category \(\mathbb{T}\), possibly equipped with extra structure
  • A model of a double theory is structure-preserving lax functor \(\mathbb{T} \to \mathbb{S}\mathsf{pan}\)

For a fixed double theory \(\mathbb{T}\), there will be a (possibly virtual) double category, even a (virtual) equipment, with:

  • objects = models of \(\mathbb{T}\)
  • arrows = morphisms of models (possibly lax, oplax, or pseudo)
  • proarrows = bimodules between models
  • cells = transformations/bimodule homomorphisms

Double-categorical logic

A new dictionary—note the level shift!

Meta-logic Double category theory
logic double theory
theory model of double theory
interpretation between theories model morphism
model of theory module/instance over model
model homomorphism module/instance homomorphism

Flavors of double theory

In order of increasing expressivity:

  1. Discrete double theories
  2. Simple double theories
  3. Cartesian double theories
  4. Finite-product double theories

Simple double theories

Definition

A simple double theory is a small, strict double category.

This is a concept with an attitude, understood as a categorified theory:

  • object = “object type”
  • arrow = “operation on objects”
  • proarrow = “morphism type”
  • cell = “operation on morphisms”
  • \(f\) = object operation with input type \(x\) and output type \(w\)
  • \(\alpha\) = morphism operation with input type \(m\) and output type \(n\)

Lambert and Patterson (2024), Section 3

Models of simple double theories

Definition

A model of a simple double theory \(\mathbb{T}\) is

  • a lax double functor \(M: \mathbb{T} \to \mathbb{S}\mathsf{pan}\), or equivalently
  • a unitary lax double functor \(M: \mathbb{T} \to \mathbb{P}\mathsf{rof}\)

Recall that unitary means that the unitors are identities (Grandis 2019, sec. 3.5.2).

Example: theory of monads

The theory of monads is the simple double theory generated by

  • an object \(x\)

  • an arrow \(t: x \to x\)

  • multiplication and unit cells

subjects to three equations expressing associativity and unitality.

Lambert and Patterson (2024), Theory 3.8

Example: theory of monads

E.g., the associativity axiom:




\[=\]

Fact

A model of the theory of monads is precisely a category \(\mathsf{C}\) along with a monad \((T,\mu,\eta)\) on \(\mathsf{C}\).

Lambert and Patterson (2024), Theory 3.8

Simple double theories, the big picture

Concept Definition
Simple double theory Small, strict double category \(\mathbb{T}\)
Model of simple double theory Lax functor \(F: \mathbb{T} \to \mathbb{S}\mathsf{pan}\)
Morphism between models (strict, pseudo, op/lax) (Strict, pseudo, op/lax) natural transformation \(\alpha: F \Rightarrow G\)
Bimodule between models Module \(M: F \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle\mid$}}\mkern-8mu{\Rightarrow}}G\)
Cell between morphisms/bimodules Modulation

Cartesian double theories, the big picture

Concept Definition
Cartesian double theory Small, cartesian, strict double category \(\mathbb{T}\)
Model of theory Cartesian lax functor \(F: \mathbb{T} \to \mathbb{S}\mathsf{pan}\)
Model morphism (strict, pseudo, op/lax) Cartesian (strict, pseudo, op/lax) natural transformation \(\alpha: F \Rightarrow G\)
Model bimodule Cartesian module \(M: F \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle\mid$}}\mkern-8mu{\Rightarrow}}G\)
Cell Modulation

Lambert and Patterson (2024), Section 6

Example: theory of pseudomonoids

The theory of pseudomonoids is the cartesian double theory generated by

  • an object \(x\)

  • arrows \(\otimes: x^2 \to x\) and \(I: 1 \to x\)

  • associator and unitor cells, along with their external inverses,

subject to two equations, the pentagon and triangle identities.

A model of the theory of pseudomonoids is a (weak) monoidal category.

Interlude: Demo

Two of the logics currently available in CatColab:

  1. Causal loop diagrams
  2. Database schemas


Try it yourself: https://catcolab.org

Warning

CatColab is pre-alpha software under active development.

Part 2: CatColab

CatColab v0.1 was developed in collaboration with:

  • Kris Brown
  • Kevin Carlson
  • Owen Lynch

I am also grateful for support from other colleagues at Topos Institute and our collaborators and funders.

See also the blog post Introducing CatColab (Carlson 2024)

Discrete double theories

Simplifying still further from simple double theories:

Definition

A discrete double theory is

  • a simple double theory having only trivial arrows and cells, or equivalently
  • a double category of the form \(\mathbb{D}\mathsf{isc}(\mathsf{B}) := \mathbb{H}(\mathsf{B})\), where \(\mathsf{B}\) is a small category

Such a double theory has only object and morphism types, no operations.

Models of discrete double theories are also known as “displayed categories” (Ahrens and Lumsdaine 2019).

Fact

A model of a discrete double theory \(\mathbb{D}\mathsf{isc}(\mathsf{B})\) is equivalent to a category sliced over \(\mathsf{B}\):

\[ \mathsf{Lax}(\mathbb{D}\mathsf{isc}(\mathsf{B}), \mathbb{S}\mathsf{pan}) \simeq \mathsf{Cat}/\mathsf{B}. \]

Causal loop diagrams

Causal loop diagrams (and also regulatory networks) are

  • signed graphs, or
  • free signed categories


Let \(\mathsf{Sgn}:= \{\pm 1\} \cong \mathbb{Z}_2\) be the group of nonzero signs.

Definition

A signed category is a category \(\mathsf{C}\) equipped with a functor \(\mathsf{C} \to \mathsf{Sgn}\).

So, the category of signed categories is the slice

\[ \mathsf{SgnCat} := \mathsf{Cat}/\mathsf{Sgn}. \]

Aduddell et al. (2024), Section 2.1

Causal loop diagrams via double theories

Theory

The theory of signed categories is the discrete double theory generated by

  • a object type \(x\)
  • a morphism type \(n: x \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle+$}}\mkern-13mu{\to}}x\) (for “negative”)

subject to the equation \(n \odot n = \mathrm{id}_x\) (where \(\mathrm{id}_x: x \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle+$}}\mkern-13mu{\to}}x\) is “positive”).

Equivalently,

\[ \mathbb{T}_{\mathsf{SgnCat}} := \mathbb{D}\mathsf{isc}(\mathsf{Sgn}), \]

so

\[ \mathsf{Lax}(\mathbb{T}_{\mathsf{SgnCat}}, \mathbb{S}\mathsf{pan}) \simeq \mathsf{Cat}/\mathsf{Sgn} = \mathsf{SgnCat}. \]

CatColab developer docs: signed categories

Free signed categories

What’s the point about thinking of signed graphs as free signed categories?

Motifs are morphisms between free signed categories, e.g.,

  • Positive/reinforcing feedback loops are morphisms out of:

  • Negative/balancing feedback loops are morphisms out of:

Aduddell et al. (2024), Section 2.2

Diagrams as free categorical structures

This phenomenon is generic:

Slogan

Diagrammatic languages are free categorical structures whenever it makes sense for arrows to compose.

A famous example:

Example

Petri nets are free symmetric/commutative monoidal categories.

Coming in a future version of CatColab!

On Petri nets and SMCS: Baez et al. (2021)

Database schemas

A basic notion of database schema is a finitely presented profunctor

where \(\mathrm{Mapping} := \mathrm{Hom}_{\mathrm{Entity}}\) and \(\mathrm{AttrOp} := \mathrm{Hom}_{\mathrm{AttrType}}\).

In SQL jargon:

  • “Entity” = table
  • “Mapping” = foreign key
  • “Attr” = data attribute = column that is not a foreign key

Schultz et al. (2017), Patterson, Lynch, and Fairbanks (2022), Roig, Meyers, and Minichiello (2024)

Schemas via double theories

Theory

The theory of profunctors is the “walking proarrow” \(\mathbb{D}\mathsf{isc}(\mathsf{2})\), a discrete double theory freely generated by

  • two objects \(0,1\)
  • one proarrow \(0 \mathrel{\mkern 3mu\vcenter{\hbox{$\scriptstyle+$}}\mkern-13mu{\to}}1\).

A model is a profunctor, either directly or indirectly via “barrels”:

\[ \mathsf{Lax}(\mathbb{D}\mathsf{isc}(\mathsf{2}), \mathbb{S}\mathsf{pan}) \simeq \mathsf{Cat}/\mathsf{2}. \]

In future versions of CatColab:

  • Database instances as modules over models of double theories
  • Algebraic databases a la Schultz et al. (2017)

Distributors and barrels on Joyal’s CatLab, esp. Proposition 2.4

Design of CatColab

  • Going from math to technology is more than just implementing a spec!
  • The embodiment of mathematics in technology requires as much creative input as the math itself

Desiderata

The system should enable formal, interoperable, conceptual modeling in domain-specific logics

  • assuming that the user knows something about a domain of interest
  • not assuming that the user knows about the meta-logical foundation

Intended users have variable levels of technical expertise and might be…

  • scientist
  • engineer
  • policy analyst
  • local expert/community leader

Structure editing

CatColab is a structure editor for categorical structures:

  • content being edited is not just a string
  • but rather a structured object (such as a model of a double theory)

Interpolates between text editors and fully graphical editors:

  • Unlike a text editor, can provide heavy scaffolding and enforce correct syntax by construction
  • Unlike a graphical editor, there seems to be hope of doing it generically across structures!

Hypothesis

It is possible and practical to build a structure editor for collaborative modeling that is ergonomic, yet parametric over the logic.

Another example is Hazel, a structure editor for functional programs (Omar et al. 2017)

User interface

We emphasize formal modeling, but informal narrative is indispensable.

CatColab has a notebook-style interface, mixing

  • formal elements handled by the structure editor
  • natural language text handled by a rich text editor

Note

Interface familiar from computational notebooks like Jupyter but very different execution model:

  • In a Jupyter notebook, cells execute individually and produce side effects
  • A CatColab notebook declaratively specifies a single structure

References

Aduddell, Rebekah, James Fairbanks, Amit Kumar, Pablo S. Ocal, Evan Patterson, and Brandon T. Shapiro. 2024. “A Compositional Account of Motifs, Mechanisms, and Dynamics in Biochemical Regulatory Networks.” Compositionality 6 (2). https://doi.org/10.32408/compositionality-6-2.
Ahrens, Benedikt, and Peter LeFanu Lumsdaine. 2019. “Displayed Categories.” Logical Methods in Computer Science 15 (1). https://doi.org/10.23638/LMCS-15(1:20)2019.
Aleiferi, Evangelia. 2018. “Cartesian Double Categories with an Emphasis on Characterizing Spans.” PhD thesis, Dalhousie University. https://arxiv.org/abs/1809.06940.
Baez, John C., Fabrizio Genovese, Jade Master, and Michael Shulman. 2021. “Categories of Nets.” In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1–13. https://doi.org/10.1109/LICS52264.2021.9470566.
Carlson, Kevin. 2024. “Introducing CatColab.” Topos Institute. 2024. https://topos.site/blog/2024-10-02-introducing-catcolab/.
Grandis, Marco. 2019. Higher Dimensional Categories: From Double to Multiple Categories. World Scientific. https://doi.org/10.1142/11406.
Grandis, Marco, and Robert Paré. 1999. “Limits in Double Categories.” Cahiers de Topologie Et géométrie Différentielle Catégoriques 40 (3): 162–220.
Lambert, Michael, and Evan Patterson. 2024. “Cartesian Double Theories: A Double-Categorical Framework for Categorical Doctrines.” Advances in Mathematics 444: 109630. https://doi.org/10.1016/j.aim.2024.109630.
Lawvere, F. William. 1963. “Functorial Semantics of Algebraic Theories.” PhD thesis, Columbia University. http://www.tac.mta.ca/tac/reprints/articles/5/tr5abs.html.
Omar, Cyrus, Ian Voysey, Michael Hilton, Joshua Sunshine, Claire Le Goues, Jonathan Aldrich, and Matthew A. Hammer. 2017. “Toward Semantic Foundations for Program Editors.” In Summit on Advances in Programming Languagess (SNAPL), 71:11:1–12. LIPIcs. https://arxiv.org/abs/1703.08694.
Paré, Robert. 2011. “Yoneda Theory for Double Categories.” Theory and Applications of Categories 25 (17): 436–89. http://www.tac.mta.ca/tac/volumes/25/17/25-17abs.html.
———. 2013. “Composition of Modules for Lax Functors.” Theory and Applications of Categories 27 (16): 393–444. http://www.tac.mta.ca/tac/volumes/27/16/27-16abs.html.
Patterson, Evan. 2024. “Products in Double Categories, Revisited.” https://arxiv.org/abs/2401.08990.
Patterson, Evan, Owen Lynch, and James Fairbanks. 2022. “Categorical Data Structures for Technical Computing.” Compositionality 4 (5). https://doi.org/10.32408/compositionality-4-5.
Roig, Gabriel Goren, Joshua Meyers, and Emilio Minichiello. 2024. “Presenting Profunctors.” https://arxiv.org/abs/2404.01406.
Schultz, Patrick, David I. Spivak, Christina Vasilakopoulou, and Ryan Wisnesky. 2017. “Algebraic Databases.” Theory and Applications of Categories 32 (16): 547–619. http://www.tac.mta.ca/tac/volumes/32/16/32-16abs.html.
Spivak, David I. 2012. “Functorial Data Migration.” Information and Computation 217: 31–51. https://doi.org/10.1016/j.ic.2012.05.001.