chore: Various minor updates relating to bicategories

[aathn]

Description

This implements @plt-amy's suggestion to replace the definitions of λ← et.c. in Cat.Bi.Base with re-exports, so that goals involving bicategory 2-cells normalise to something nicer. I also add ⊗ as an alias for the module compose to the same effect. The former change means α← and α→ now need to have their arguments passed as a tuple, but I would argue it's worth it to get the nicer normal forms, especially since these arguments are often omitted anyways.

(The analogue of these changes could also be applied monoidal categories, but I left them unchanged for now.)

In addition, I redefine the preaction and postaction functors using Bifunctor.Left and Bifunctor.Right, to make them compatible with the unitors, and add no-eta-equality to the various bicategory-related records.

Update: I also did the re-export thing for γ→, ν→ etc, and added naturality shorthands γ→nat, ν→nat, etc.

Checklist

Before submitting a merge request, please check the items below:

• I've read the contributing guidelines.
• The imports of new modules have been sorted with support/sort-imports.hs (or nix run --experimental-features nix-command -f . sort-imports).
• All new code blocks have "agda" as their language.

If your change affects many files without adding substantial content, and
you don't want your name to appear on those pages (for example, treewide
refactorings or reformattings), start the commit message and PR title with chore:.

[plt-amy]

Thanks!

[plt-amy]

Do you mind if this is merged before #606 ?

[Lavenza]

Pull request preview

Changed pages

• Cat.Bi.Base (+93, -76)
• Cat.Bi.Diagram.Monad (± 13)

[aathn]

I don't mind at all :)