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.

[Patrick Nicodemus]

I reached out to Mike Shulman about his paper and asked him if he had any comments about what a good general definition is.

Good question! My instinct would be that the best definition of weak double category to use in a proof assistant would be what Aaron and I called a "tidy double bicategory" -- Verity's definition plus a "saturation" axiom to ensure the bigons are determined by the squares.
In addition to being finitary, which is an advantage for formalization, this has the advantage that the horizontal and vertical bicategories are explicitly part of the structure. Thus, for instance, if you build a weak double category of quintets from a bicategory, then the horizontal and vertical bicategories of that double category could be definitionally equal to the bicategory you started from.

[Robin Carlier]

So it seems from this that the definition would indeed have to go first from Verity's double bicategories, and then specialize from there on. This is probably a rather big project.

[Kevin Buzzard]

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

PSA: when posting a large amount of code, I've noticed that Zulip sometimes adds extra newlines in between each line. One can fix this by hitting ctrl-Z ("undo") after the pasting (which, counterintuitively, doesn't delete it; it just deletes all the extra incorrect formatting). It's a bit like when you copy and paste a declaration name from the mathlib docs; at the paste the URL is sometimes pasted too, but you can remove it with ctrl-Z.

tl;dr @Patrick Nicodemus try editing your original post, copy the lean code as before from VS Code or whatever, paste it, and then if there are still blank lines on every second line, hit Ctrl-Z (or Command-Z on a mac) and see if this fixes it.

[Yaël Dillies]

Kevin Buzzard said:

when posting a large amount of code, I've noticed that Zulip sometimes adds extra newlines in between each line

It's not about the amount. It's about whether you are pasting it in a code block

[Patrick Nicodemus]

@Robin Carlier I thought about this a little more and I wanted to explain where some of the casts come from. My design involves something that is very similar to that of a displayed category. If you think about how a displayed category works, if the base category is a normal category then the associativity of composition in the total category is only well-typed by casting along the associativity in the base category, and same with left and right identities. There are various ways to get around this - using heterogeneous equality or an equality between morphisms in the total space that "rides" a morphism in the base space - but all of them seem kind of equivalent to me.
One could pass to a 2-categorical version of displayed categories but that seems to just shift the problem up one degree.

Does this make sense? Do you think casting is justified from the perspective of "this is essentially a displayed category and these casts are coming from the need for associativity in the total category to be well-formed"?

[Robin Carlier]

I understand why casts appears in this situation, though I do not know a lot about displayed categories.
To repeat why I am slightly wary of casts here: they make definitions possible but my experience is that more often than not, they do not make working with the definition pleasant at all. It works at first, but it hardly scales.

To make composition well-formed while hiding away the casts, a trick that has been used in Mathlib is to carry around equality proof as parameters to control the return type of compositions. for instance, you field comp would look like this

-- ...
  /-- 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''}
  {f'' : c ⟶ c''} {g'' : d ⟶ d''} (e₁ : f ≫ f' = f'') (e₂ : g ≫ g' = g'')
  {X : HHom c d} {Y : HHom c' d'} {Z : HHom c'' d''} :
  □(f,g; X, Y) → □(f', g'; Y, Z) → □(f'', g''; X, Z)

Similarly, the identity field could depend on a pair of morphisms that are equal to the identities.

This pattern has been used in mathlib for working with pseudofunctors out of strict (e.g locally discrete) bicategories and works quite well for this.

[Robin Carlier]

Also, I didn’t do it in the snippet above, but one nice thing about adding these equality params is that you can add autoparameters for them (grind, cat_disch, ...) so that they are discharged automatically. This way you can write most morphisms as you wold normally without having to feed it Category.id_comp, Category.assoc etc. manually all the time