Bicat of bimods

[tillrampe]

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.

[tillrampe]

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 𝒞.

[tillrampe]

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]

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.

[tillrampe]

There is still a lot more to change, but at least the variable names in TensorproductOfBimodules and TensorproductOfHomomorphisms are improved. They are hopefully clearer now, and many of them are used in other files as projections without renaming. You are invited to revisit the two aforementioned files and give feedback on the variable names.

[tillrampe]

I will be rather busy until beginning of October. So, I might not be able to make changes to this pull request. I will finish this, however, as soon as my schedule allows.

[JacquesCarette]

Thanks for letting me know. Would it be worth my re-reviewing this in the mean time?

[tillrampe]

Don't think so. I've mainly executed the changes we agreed were necessary before; like using push, pull, etc. from Morphism.Reasoning to shorten proofs, and not renaming fields of Bimodule and Monad instances.

[tillrampe]

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

[JacquesCarette]

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]

(closing and reopening to get CI to run)

[JacquesCarette]

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 _⊗₁_)

[JacquesCarette]

ping: could you look at the build failure please?