Bicat of bimods #482

tillrampe · 2025-07-21T10:58:50Z

This pull request constructs the bicategory of monads and bimodules (cf. Shulman - Framed Bicategories and Monoidal Fibrations, Ch. 11). This is the result that the previous pull requests have been leading up to.

Bring the changes to cat-of-bimods made during the revision process to bicat-of-bimods

… with a 1-cell

…r moving it to a different file

…local coequalizers with 1-cells

…rs with a 1-cell

… with a 1-cell

… its definition around

…Construction.Bimodules.Properties.agda as they have been renamed

…r with a 1-cell

…a local coequalizer with a 1-cell

tillrampe · 2025-07-21T11:43:01Z

As of now, this pull request type-checks, but it will need revision. Among the things to improve are:

Don't import in where-clauses.
Use using-commands wherever feasible.
Don't open multiple instances of a module. Use projections instead. (I want to rename many variables in Categories.Bicategory.Construction.Bimodules.Tensorproduct and refer to the involved bimodules as L and R for 'left' and 'right'.)
Split Categories.Bicategory.Construction.Bimodules.Tensorproduct into two files: TensorproductOfBimodules.agda and TensorproductOfHomomorphisms.agda
Use Categories.Bicategory.Monad.Bimodule.bimodHelper to define the tensorproduct of bimodules.
eta-reduce where possible

These should be the major style requests made during the previous revision processes. Let me know if I forgot any.
I want to continue writing the tensorproduct of bimodules in function composition order. Although unusual in the algebra literature, it is more import to follow the order of composition in the bicategory 𝒞.

JacquesCarette

Right about the changes that need done. I suggest a few more.

Overall: heroic work! Very impressive.

JacquesCarette · 2025-07-21T18:54:08Z

src/Categories/Bicategory/Construction/Bimodules.agda

@@ -0,0 +1,82 @@
+{-# OPTIONS --without-K --safe --lossy-unification  #-}


revisit --lossy-unification (just in case it is no longer needed)

JacquesCarette · 2025-07-21T18:55:26Z

src/Categories/Bicategory/Construction/Bimodules.agda

+
+open import Categories.Bicategory.Monad.Bimodule
+import Categories.Category.Construction.Bimodules
+open Categories.Category.Construction.Bimodules {o} {ℓ} {e} {t} {𝒞} renaming (Bimodules to Bimodules₁)


Renaming to a name with a subscript is rarely clear. Please try to rename to something more conceptual.

The 1 in Bimodules₁ stands for 1-category. Isn't that conceptual already? I could rename it to 1CatOfBimodules or similar, but I'm not sure that improves readability. Further, the file Categories.Bicategory.Construction.Span.agda follows the same naming convention.

Sometimes things slip through, and I don't notice that it's a sub-optimal convention.

What about 1-Bimodules, which is closer to what people in category theory do?

JacquesCarette · 2025-07-21T18:56:22Z

src/Categories/Bicategory/Construction/Bimodules.agda

+open import Categories.Bicategory
+open import Categories.Bicategory.LocalCoequalizers
+
+module Categories.Bicategory.Construction.Bimodules {o ℓ e t} {𝒞 : Bicategory o ℓ e t} {localCoeq : LocalCoequalizers 𝒞} where


Surprised that the last argument is implicit. If that's actually fine, that's probably worth a comment!

JacquesCarette · 2025-07-21T18:57:35Z

src/Categories/Bicategory/Construction/Bimodules.agda

+
+Bimodules : Bicategory (o ⊔ ℓ ⊔ e) (ℓ ⊔ e) e (o ⊔ ℓ ⊔ e ⊔ t)
+Bimodules = record
+  { enriched = record


I think it would make sense to pull the 'enriching base' out as its own definition. It might even belong elsewhere?

JacquesCarette · 2025-07-21T19:01:24Z

src/Categories/Bicategory/Construction/Bimodules/Tensorproduct.agda

+      sq₁ : CommutativeSquare (F₂∘₁T₂▷actionˡ₁) ((act-to-the-left) ◁ T₁) (act-to-the-left) (F₂▷actionˡ₁)
+      sq₁ = begin
+        act-to-the-left ∘ᵥ F₂∘₁T₂▷actionˡ₁                                     ≈⟨ refl⟩∘⟨ sym-assoc₂ ⟩
+        F₂ ▷ actionʳ₁ ∘ᵥ (associator.from ∘ᵥ (F₂ ∘₁ T₂) ▷ actionˡ₁)


like in previous files, the shorthands for the associators make a big different on length.

JacquesCarette · 2025-07-21T19:02:53Z

src/Categories/Bicategory/Construction/Bimodules/Tensorproduct.agda

+      identityˡ-triangle : F₂▷actionˡ₁ ∘ᵥ (F₂ ∘₁ F₁) ▷ η₁ ∘ᵥ unitorʳ.to ≈ id₂
+      identityˡ-triangle = begin
+        F₂▷actionˡ₁ ∘ᵥ (F₂ ∘₁ F₁) ▷ η₁ ∘ᵥ unitorʳ.to ≈⟨ assoc₂ ⟩
+        F₂ ▷ actionˡ₁ ∘ᵥ associator.from ∘ᵥ (F₂ ∘₁ F₁) ▷ η₁ ∘ᵥ unitorʳ.to ≈⟨ refl⟩∘⟨ sym-assoc₂ ⟩


line up the justifications

JacquesCarette · 2025-07-21T19:04:25Z

src/Categories/Bicategory/Construction/Bimodules/Tensorproduct.agda

+
+      identityˡ∘arr : (actionˡ ∘ᵥ F ▷ η₁ ∘ᵥ unitorʳ.to) ∘ᵥ Coequalizer.arr F₂⊗F₁ ≈ id₂ ∘ᵥ Coequalizer.arr F₂⊗F₁
+      identityˡ∘arr = begin
+        (actionˡ ∘ᵥ F ▷ η₁ ∘ᵥ unitorʳ.to) ∘ᵥ Coequalizer.arr F₂⊗F₁ ≈⟨ assoc₂ ⟩


looks like there is a lot of 'refocusing' steps that can often be dealt with with push/pull. Definitely worth trying, so that the 'heart' of the proof becomes easier to see.

JacquesCarette · 2025-07-21T19:10:29Z

src/Categories/Bicategory/Construction/Bimodules/Tensorproduct/Associator.agda

+  open Bimodule B₁ using () renaming (actionˡ to actionˡ₁)
+
+  abstract
+    linearˡ∘arr∘arr : ((Bimodule.actionˡ (B₃ ⊗₀ B₂ ⊗₀ B₁)


Is the 'shape' of this lemma forced? It's always odd when the first N steps (and last K steps) are all assoc-shuffling.

JacquesCarette · 2025-07-21T19:13:49Z

src/Categories/Bicategory/Construction/Bimodules/Tensorproduct/Associator/Naturality.agda

+      open TensorproductOfHomomorphisms (f₃ ⊗₁ f₂) f₁ renaming (αSq to αSq[f₃⊗f₂]⊗f₁)
+      open TensorproductOfHomomorphisms f₃ (f₂ ⊗₁ f₁) renaming (αSq to αSqf₃⊗[f₂⊗f₁])
+
+  α⇒⊗-natural∘arr : (α⇒⊗ {B₃'} {B₂'} {B₁'}


consider formatting like

foo : term1 ≈ term2

and similarly for equalities, i.e. don't indent by 20+ but instead by 2. And for this stuff, a width limit of 120 is probably fine (instead of just 80).

JacquesCarette · 2025-07-21T19:15:36Z

src/Categories/Bicategory/Construction/Bimodules/Tensorproduct/Coherence/Pentagon.agda

+    ∘ᵥ Coequalizer.arr [[F₄⊗F₃]⊗F₂]⊗F₁
+    ∘ᵥ Coequalizer.arr [F₄⊗F₃]⊗F₂ ◁ F₁
+    ∘ᵥ Coequalizer.arr F₄⊗F₃ ◁ F₂ ◁ F₁
+    ≈⟨ sym-assoc₂ ⟩


have you experimented with indenting the justification lines a lot more? Since these are all quite short, you could create a 2-column view (but keep the first column as you have it.)

I've just tried it. It looks decent.

tillrampe · 2025-07-28T09:43:02Z

I am considering changing the directional indicators ˡ and ʳ as in actionʳ and actionˡ from diagrammatic order to algebraic order. Algebraic order seems to be the common choice in this library. However, the definition of monads stands out as having diagrammatic ordering in the naming convention (see indentityˡ and identityʳ). What do you advise?

JacquesCarette · 2025-07-28T14:31:40Z

We were too busy just creating the library to pay (enough) attention to being systematic about right/left, algebraic vs diagrammatic order, etc. (Same happened with stdlib and we're suffering because of it now.)

So I wouldn't worry too much about you being consistent with the library, since there is no explicit design decision on that front (yet!).

I think a lot of the choices in the library were non-choices, in the sense that they followed older / naive categorical writing. And that often used algebraic order. Whereas I think that more modern approaches are shifting to diagrammatic order!

If you're on the category theory Zulip, that might be an interesting question to ask there.

…his name in other files as projection without renaming command

… to reserve the name F for the projection of the bimodule record field

tillrampe · 2025-10-28T20:09:40Z

This is ready for re-review now. It all type checks on my device.

JacquesCarette · 2025-10-29T17:21:35Z

Will re-review soon. It might still be blocked because the CI is currently broken! I've been wanting to fix that, but have not had the time for that either.

JacquesCarette · 2025-11-16T16:35:25Z

(closing and reopening to get CI to run)

JacquesCarette · 2025-11-16T16:46:01Z

Build failed with

/home/runner/work/agda-categories/agda-categories/src/Categories/Bicategory/Construction/Bimodules/TensorproductOfHomomorphisms.agda:98.5-64: warning: -W[no]OpenImportAbstract
`abstract' does not have any effect on `open' so better place this
statement outside of the abstract block
when scope checking the declaration
  open import Categories.Bicategory.Construction.Bimodules.TensorproductOfHomomorphisms using ()
                                                                                        renaming (Tensorproduct to infixr 30 _⊗₁_)

tillrampe added 18 commits May 30, 2025 20:35

Construct the bicategory of monads and bimodules

b6cdcb4

Merge branch 'cat-of-bimods' into bicat-of-bimods

ad429e2

Bring the changes to cat-of-bimods made during the revision process to bicat-of-bimods

Update the names of the functions that pre-/postcompose a coequalizer…

3df42f3

… with a 1-cell

Bring Bimodulehomomorphism into scope, this has become necessary afte…

e6f9e1a

…r moving it to a different file

Give a name to the module that contains functions pre-/postcomposing …

510d38e

…local coequalizers with 1-cells

Bring the functions into scope that pre-/postcompose local coequalize…

3d98456

…rs with a 1-cell

Open functions in the order they have been defined (purely aesthetical)

2f2b519

Update the names of the functions that pre-/postcompose a coequalizer…

ca939d5

… with a 1-cell

Bring Bimodulehomomorphism into scope, this is necessary after moving…

d81253c

… its definition around

Update names of functions and modules defined in Categories.Category.…

a65c7a6

…Construction.Bimodules.Properties.agda as they have been renamed

Update name of the functions that pre-/postcompose a local coequalize…

9dfa804

…r with a 1-cell

Update the file according to the renamings made in the revision process

1a514f1

Import Bimodulehomomorphism, it is under a new path now

0964da1

Update names according to changes made during the revision process

5e7e491

Import Bimodulehomomorphism, it isnow under a new path

d428347

Declare the presendence of the infix operators that pre-/postcompose …

8ce1c30

…a local coequalizer with a 1-cell

Update names according to changes made during revision process

0ce44c1

Update names according to changes made during revision process

598e34e

JacquesCarette requested changes Jul 21, 2025

View reviewed changes

tillrampe added 2 commits July 24, 2025 12:38

Split Tensorproduct.agda into two files

c354847

Fix typo in comment

0cb626c

tillrampe force-pushed the bicat-of-bimods branch from bbe8850 to 2dba97e Compare July 29, 2025 15:33

tillrampe added 5 commits July 30, 2025 12:42

Improve the list of files that git ignores

b16c012

Rename the coequalizer created by two composable bimodules, and use t…

bd1b304

…his name in other files as projection without renaming command

Remove unnecessary open commands

1bc8734

Improve comments in the construction of the tensorproduct

19cdb96

Rename the underlying two cell of the tensorproduct bimodule; we want…

592f9e1

… to reserve the name F for the projection of the bimodule record field

tillrampe added 24 commits October 24, 2025 15:44

Improve import commands

ae3b3d3

Shorten notation by opening Coequalizer

fa94fba

Use Morphism.Reasoning to shorten proofs

b11d67b

Use Shorthands in Extras to shorten name for associator

6fba10b

Don't rename fields, use them as projections instead

67eae25

Shorten notation by opening record types

06bbad3

Improve import open commands in the preamble

22aac4d

Rename proofs to be consistent with other files in the project

4f031f8

Shorten proof using Categories.Morphism.Reasoning

0d545ff

Improve indentation

ee8238f

Remove line break

2c790f4

Shorten notation by opening modules

bae32a5

Adapt to the new name in Pentagon.agda

e698ca6

Shorten proofs by using Morphism.Reasoning

1163647

Add lemmata about long squares being preserved by whiskering

4a3a47c

Impove line breaks and indentation

585637f

Introduce a shorthand for the tensor product whiskering

fa5e89f

Move open import commands to the preamble

59e4909

Improve import commands by not using alias'

c61b179

Change the name for the 1-category of bimodules

2b6518b

Remove unnecessary white space

590bd9c

Specify open command by a using qualifier

cc45b69

Improve indentation

e4f1326

Improve import preamble

931810b

JacquesCarette closed this Nov 16, 2025

JacquesCarette reopened this Nov 16, 2025

		@@ -0,0 +1,82 @@
		{-# OPTIONS --without-K --safe --lossy-unification #-}

Bicat of bimods #482

Are you sure you want to change the base?

Bicat of bimods #482

Uh oh!

Conversation

tillrampe commented Jul 21, 2025

Uh oh!

tillrampe commented Jul 21, 2025

Uh oh!

JacquesCarette left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tillrampe commented Jul 28, 2025

Uh oh!

JacquesCarette commented Jul 28, 2025

Uh oh!

tillrampe commented Oct 28, 2025

Uh oh!

JacquesCarette commented Oct 29, 2025

Uh oh!

JacquesCarette commented Nov 16, 2025

Uh oh!

JacquesCarette commented Nov 16, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants