Proposal: Double categories in mathlib

Stream: mathlib4

[Patrick Nicodemus]

I am interested in contributing the definition of a weak double category to mathlib, and examples.

I started writing it down and I feel that it would be better to refactor the existing definition of bicategory to make it more modular.

I will include my code so far below, which indicates the design definition I want to go.

import Mathlib.CategoryTheory.Category.Basic

import Mathlib.CategoryTheory.Bicategory.Basic

import Mathlib.CategoryTheory.Category.Cat

import Mathlib.CategoryTheory.Functor.Basic

open CategoryTheory

section ParametricQuiver

set_option linter.unusedVariables false

class hzQuiver.{v1, u1} (O : Type u1) where

HHom : O -> O -> Type v1

class ParametricQuiver.{v₁, u₁, v₂, u₂, v₃, u₃}

(O₁ : Type u₁) [Quiver.{v₁} O₁] (O₂ : Type u₂) [Quiver.{v₂} O₂]

(HHom : O₁ -> O₂ -> Type u₃) where

two_cells : forall {o₁ o₁' : O₁} (f : Quiver.Hom o₁ o₁') {o₂ o₂' : O₂} (g : Quiver.Hom o₂ o₂'),

HHom o₁ o₂ -> HHom o₁' o₂' -> Sort v₃

end ParametricQuiver

section ParametricCategory

universe u₁ v₁ u₂ v₂ w₁ w₂

open ParametricQuiver in

/--

A parametric CategoryStruct over two CategoryStructs C and D.
- For each pair of objects (c, d) in C × D, we have a type of objects Ob c d
- For each pair of morphisms (f : c → c') in C and (g : d → d') in D,

and objects X : Ob c d and Y : Ob c' d', we have a type of morphisms Hom f g X Y
-/

local notation:50 "□(" f "," g ";" X "," Y ")" => two_cells f g X Y

class ParametricCategoryStruct (C : Type u₁) (D : Type u₂)

[Ccat : CategoryStruct.{v₁, u₁} C] [Dcat: CategoryStruct.{v₂,u₂} D]

(HHom : C -> D -> Type w₁) [ParametricQuiver.{v₁ + 1, u₁, v₂ + 1, u₂, w₂ + 1, w₁} C D HHom]

: Type (max u₁ v₁ u₂ v₂ w₁ w₂ + 1) where

/-- Identity morphism over the pair of identity morphisms -/

id : ∀ {c : C} {d : D} (F : HHom c d), ParametricQuiver.two_cells (𝟙 c) (𝟙 d) F F

/-- Composition of morphisms over composition of base morphisms -/

comp : ∀ {c c' c'' : C} {d d' d'' : D}

{f : c ⟶ c'} {f' : c' ⟶ c''} {g : d ⟶ d'} {g' : d' ⟶ d''}

{X : HHom c d} {Y : HHom c' d'} {Z : HHom c'' d''},

□(f,g; X, Y) → □(f', g'; Y, Z) → □( (f ≫ f'), (g ≫ g'); X, Z)

def special2cell {C : Type u₁} {D : Type u₂} [Category C] [Category D]

(HHom : C -> D -> Type v₁)

[ParametricQuiver _ _ HHom]

[ParametricCategoryStruct C D HHom] {x : C} {y : D}

(f g : HHom x y) :=

□(𝟙 x, 𝟙 y; f, g)

/--

A parametric Category over two Categories C and D.

Extends ParametricCategoryStruct with identity and associativity axioms.

These axioms state that the parametric structure respects the categorical structure of C and D.
-/

class ParametricCategory (C : Type u₁) (D : Type u₂)

[Category.{v₁} C] [Category.{v₂} D]

(HHom : C -> D -> Type w₁)

[ParametricQuiver _ _ HHom]

extends ParametricCategoryStruct.{u₁, v₁, u₂, v₂, w₁, w₂} C D HHom where

/-- Identity morphisms are left identities for composition,

modulo the left identity laws in C and D -/

id_comp : ∀ {c c' : C} {d d' : D} {f : c ⟶ c'} {g : d ⟶ d'}

{X : HHom c d} {Y : HHom c' d'} (h : □(f, g; X, Y)),

(Category.id_comp f) ▸ (Category.id_comp g) ▸ (comp (id X) h) = h
-- ((Category.id_comp f).symm ▸ (Category.id_comp g).symm ▸ h : □((𝟙 c ≫ f), (𝟙 d ≫ g); X, Y))

/-- Identity morphisms are right identities for composition,

modulo the right identity laws in C and D -/

comp_id : ∀ {c c' : C} {d d' : D} {f : c ⟶ c'} {g : d ⟶ d'}

{X : HHom c d} {Y : HHom c' d'} (h : □(f, g; X, Y)),

(Category.comp_id f) ▸ (Category.comp_id g) ▸ comp h (id Y) = h

/-- Composition is associative, modulo the associativity laws in C and D -/

assoc : ∀ {c₀ c₁ c₂ c₃ : C} {d₀ d₁ d₂ d₃ : D}

{f₁ : c₀ ⟶ c₁} {f₂ : c₁ ⟶ c₂} {f₃ : c₂ ⟶ c₃}

{g₁ : d₀ ⟶ d₁} {g₂ : d₁ ⟶ d₂} {g₃ : d₂ ⟶ d₃}

{X : HHom c₀ d₀} {Y : HHom c₁ d₁} {Z : HHom c₂ d₂} {W : HHom c₃ d₃}

(h₁ : □(f₁, g₁; X,Y)) (h₂ : □(f₂, g₂; Y, Z)) (h₃ : □(f₃, g₃; Z, W)),

comp (comp h₁ h₂) h₃ =

(Category.assoc f₁ f₂ f₃ ▸ Category.assoc g₁ g₂ g₃ ▸

comp h₁ (comp h₂ h₃) : □((f₁ ≫ f₂) ≫ f₃, (g₁ ≫ g₂) ≫ g₃; X, W))

instance special2cellCatStruct.{u, v} (C : Type u) (D : Type v) [Category C] [Category D]

(HHom : C -> D -> Type w₁)

[ParametricQuiver C D HHom]

[ParametricCategoryStruct C D HHom] {x : C} {y : D}

: CategoryStruct (HHom x y) := {

Hom := special2cell HHom

id := ParametricCategoryStruct.id

comp := fun {X Y Z} (f : special2cell HHom X Y) (g : special2cell HHom Y Z) =>

(Category.comp_id (𝟙 x) ▸ Category.comp_id (𝟙 y) ▸

ParametricCategoryStruct.comp f g :

□(𝟙 x, 𝟙 y; X, Z))

}

open ParametricCategoryStruct in

instance special2cellCat.{u} (C : Type u) [Category C]

(D : Type v) [Category D]

(HHom : C -> D -> Type w₁)

[ParametricQuiver _ _ HHom]

[ParametricCategory C D HHom] {x : C} {y : D}

: Category (HHom x y) := {

id_comp := fun {X Y} f => by

dsimp [CategoryStruct.comp, special2cellCatStruct]

exact ParametricCategory.id_comp f

comp_id := fun {X Y} f => by

dsimp [CategoryStruct.comp, special2cellCatStruct]

exact ParametricCategory.comp_id f

assoc := fun {W X Y Z} f g h => by

dsimp [CategoryStruct.comp, special2cellCatStruct]

apply (congr_arg (fun z => (@Eq.rec

(x ⟶ x) (𝟙 x ≫ 𝟙 x) (fun x_1 h ↦ □(x_1,𝟙 y;W,Z))

z

(𝟙 x) (special2cellCatStruct._proof_1 C) : □(𝟙 x,𝟙 y;W,Z))))

apply (congr_arg (fun z => (@Eq.rec (y ⟶ y) (𝟙 y ≫ 𝟙 y) (fun x_1 h ↦ □(𝟙 x ≫ 𝟙 x,x_1;W,Z))

z (𝟙 y) (special2cellCatStruct._proof_1 D) : □(𝟙 x ≫ 𝟙 x,𝟙 y;W,Z))))

apply eq_of_heq

apply (HEq.trans (b := comp (comp f g) h))

{ grind }

apply (HEq.trans (b := comp f (comp g h)))

{ grind [ParametricCategory.assoc] }

grind

}

class DoubleCategoryStruct.{uob, uv, uh, u2} (C : Type uob) [Category.{uv} C]

(HHom : C -> C -> Type uh) [ParametricQuiver _ _ HHom]

extends ParametricCategory.{uob, uv, uob, uv, uh, u2} C C HHom where

/-- Horizontal identity object: for each vertical object c, we have an identity object -/

horiz_id : ∀ {c : C}, HHom c c

/-- Horizontal composition of objects -/

horiz_comp : ∀ {c c' c'' : C}, HHom c c' → HHom c' c'' → HHom c c''

/-- Horizontal identity 2-cell: for each vertical morphism, we have an identity 2-cell -/

horiz_id_2cell : ∀ {c c' : C} (f : c ⟶ c'), ParametricQuiver.two_cells f f horiz_id horiz_id

/-- Horizontal composition of 2-cells: compose 2-cells with the same left and right sides -/

horiz_comp_2cell : ∀ {c c' c'' d d' d'' : C}

{f : c ⟶ d} {f' : c' ⟶ d'} {f'' : c'' ⟶ d''}

{X : HHom c c'} {Y : HHom c' c''} {X' : HHom d d'} {Y' : HHom d' d''},

ParametricQuiver.two_cells f f' X X' → ParametricQuiver.two_cells f' f'' Y Y' →

ParametricQuiver.two_cells f f'' (horiz_comp X Y) (horiz_comp X' Y')

/-- Horizontal composition of identity 2-cells is the identity 2-cell on the composite -/

horiz_comp_id : ∀ {c₀ c₁ c₂ : C} (X : HHom c₀ c₁) (Y : HHom c₁ c₂),

horiz_comp_2cell (id X) (id Y) =

id (horiz_comp X Y)

/-- Interchange law: horizontal composition respects vertical composition -/

interchange : ∀ {c₀ c₁ c₂ d₀ d₁ d₂ e₀ e₁ e₂ : C}

{f₁ : c₀ ⟶ d₀} {f₂ : d₀ ⟶ e₀} {g₁ : c₁ ⟶ d₁} {g₂ : d₁ ⟶ e₁}

{h₁ : c₂ ⟶ d₂} {h₂ : d₂ ⟶ e₂}

{X : HHom c₀ c₁} {Y : HHom c₁ c₂} {X' : HHom d₀ d₁} {Y' : HHom d₁ d₂}

{X'' : HHom e₀ e₁} {Y'' : HHom e₁ e₂}

(α : ParametricQuiver.two_cells f₁ g₁ X X') (β : ParametricQuiver.two_cells g₁ h₁ Y Y')

(γ : ParametricQuiver.two_cells f₂ g₂ X' X'') (δ : ParametricQuiver.two_cells g₂ h₂ Y' Y''),

horiz_comp_2cell (comp α γ) (comp β δ) =

comp (horiz_comp_2cell α β) (horiz_comp_2cell γ δ)

end ParametricCategory

In natural language, my idea is to start with a category of objects and horizontal arrows. (For example, the category of rings and ring homomorphisms.) we then introduce a notion of "parametric category", which is essentially a span in the category of categories but presented in a displayed style. (For example, the category of triples (R,S, M) where M is an (R,S)-bimodule, and morphisms (phi, psi, f) where phi, psi are ring homomorphisms and f is a (phi,psi)-equivariant map.)

Then, we would want to add vertical composition (for example tensoring of modules). I think it is best to view this as a bicategory structure enriching the data we have so far. Then we have to add vertical composition of 2-cells, which I view as a kind of parametric bicategory structure which rides the existing bicategory structure on bimodules.

[Patrick Nicodemus]

I will also invite guidance on what is the appropriate size of a pull request, say measured in 100s of lines of code.

[Patrick Nicodemus]

I started writing it down and I feel that it would be better to refactor the existing definition of bicategory to make it more modular.

I am aware that there are performance problems from decomposing the typeclass structure hierarchy too finely, so I think sophisticated guidance on this point would be appreciated. I think that Coq's math-comp library has an interesting approach of controlled code duplication where many definitions are given in both a bundled and unbundled style.

[Robin Carlier]

It seems indentation got lost in your copy-pasting in the backtick, this makes things hard to read.
You mention refactoring bicategories: can you precise what you’d like to refactor?
Right now, the focus of category theory in mathlib favors way, way more the unbundled designs over the bundled ones (one of the reason being that it allows for more universe polymorphism).

[Robin Carlier]

At a glance, it also seems you are fighting with casts in ParametricCategory and ParametricCategoryStruct: we usually try to avoid direct casts like the plague in mathlib category theory. When they are "really needed", we use eqToHom and eqToIso as wrapper around them.

[Robin Carlier]

I really like mathlib's design to start with the weakest possible structure (bicategories) to have no problems with "casting" like this, and then specialize this weakest possible object to a "strict version" (2-categories in mathlib are not directly defined, and instead, we have docs#CategoryTheory.Bicategory.Strict as a typleclass on a bicategory asserting that "it’s a 2-category"). In the case of 2-categories vs bicategories, the "weak concept" is rather common and well-known, but I’m much less aware of the "fully weak" version of double categories in the literature for ordinary categories, so I am not sure how viable is this option (it stills feels like the "morally correct" option IMO).

[Joël Riou]

The concept of bicategory is quite standard, and we already have significant code using this notion. Then, I am a little bit worried with your suggestion to "refactor the existing definition of bicategory".

[Patrick Nicodemus]

Joël Riou said:

The concept of bicategory is quite standard, and we already have significant code using this notion. Then, I am a little bit worried with your suggestion to "refactor the existing definition of bicategory".

I didn't intend to suggest redefining the meaning of bicategory to have a different semantic meaning that conflicts with the standard textbook definition. What I mean is that the current typeclass hierarchy for bicategories is only two levels deep:

• level 1: CategoryStruct, which contains Ob, Hom, comp, id
• level 2: everything else

There are various reasons you might want to decompose level 2 into multiple levels. For example, if there is a natural diamond shape in the structure hierarchy A -> B -> D and A -> C -> D, then it would be ideal if B and C contain no overlap, otherwise in trying to define a D you have to say that the data contained in B and C is equivalent or identical, or else define B' which captures some, but not all, of the theory in B.

The definitions of weak double category and bicategory contain substantial overlap, so there has to be some thought about how to organize this. I won't insist on modifying current code but in that case there will be a healthy amount of code duplication.

[Patrick Nicodemus]

Right now, the focus of category theory in mathlib favors way, way more the unbundled designs over the bundled ones (one of the reason being that it allows for more universe polymorphism).

To clarify, I mean bundled/unbundled as a spectrum, not a binary. The current definition of a bicategory involves only two typeclasses, which I consider to be more toward the "bunded" side. If I had an arbitrary 2-graph and I could say "now, furthermore, assume this 2-graph is equipped with a bicategory structure", then that would be moving a bit more in the unbundled direction, but that appears to be not possible with the current design.

[Patrick Nicodemus]

Robin Carlier said:

At a glance, it also seems you are fighting with casts in ParametricCategory and ParametricCategoryStruct: we usually try to avoid direct casts like the plague in mathlib category theory. When they are "really needed", we use eqToHom and eqToIso as wrapper around them.

I see where you are coming from from a broad perspective of starting with the weakest possible structure and specializing to a strict one, and I can understand that perspective.
Dominic Verity has discussed a concept of "doubly weak double category" which is weak in both directions, I can't say I'm really familiar with this notion or have seen it used in the literature, or am familiar with many examples of it. It's possible that this would just be inflating the complexity of the formalization effort by introducing unnecessary generality.
https://ncatlab.org/nlab/show/double+category#double_bicategories

Conceptually, I suppose we can think of casts as just transport in an isofibration over a thin groupoid; as a practical matter, code written for Prop cannot directly translate to code for Type, and so literally proving things for an isofibration would be generalizeable in ways that code in Prop cannot. But in this case I personally have no interest in the extra generality given by doubly weak bicategories, maybe somebody else will come along with interesting applications of these structures and why they deserve to be included in Mathlib.

[Patrick Nicodemus]

Robin Carlier said:

It seems indentation got lost in your copy-pasting in the backtick, this makes things hard to read.

Yes, thank you. I will upload the file independently later.

[Robin Carlier]

(From a quick search, it seems Fairbanks and Shulman also worked on variants of double categories where everything is weak: https://arxiv.org/pdf/2506.23651. Proposition 7.22 claims to give a finite description of what something "weak in both direction" should be.
I do agree that this is not a notion that one encounters a lot in the literature (at least in "lower-dimensional" category theory like this; I’ve seen a few times double ∞-categories (which must be fully weak everywhere) show up in the ∞-categorical literature, but mathlib is definitely not ready for this yet).

[Patrick Nicodemus]

To be a bit more precise about the refactoring of bicategories, if we consider the double category of rings, ring homomorphisms and bimodules, there are two bicategories involved here:

• a bicategory of rings, and bimodules between rings, with composition given by the tensor product
• a bicategory whose objects are ring homomorphisms (f_R : R1 -> R2), whose 1-cells are pairs of bimodules (M an (R1, S1)-bimodule, N an (R2, S2)-bimodule) together with an (f_R, g_R)-equivariant homomorphism M -> N; a 2-cell (M, N, phi: M -> N) => (M', N', psi) would be a pair of ring homomorphisms s: M -> M' and t :N-> N' such that t\circ phi = psi \circ s

The coherence laws for a weak double category are largely subsumed by requiring that both of these are bicategories and the src and target projections are strict functors preserving all the bicategory structure on the nose. That is why I want to talk about "a bicategory structure on the given data"; the existing definition of bicategory seems too bundled to facilitate this.