Opposite monoidal categories and related duality

[jajaperson]

Description

Extending #575, this pull request defines the following

• Isomorphism of categories $(\mathcal C \times \mathcal D)^\mathrm{op} \cong \mathcal C^\mathrm{op} \times \mathcal D^\mathrm{op}$
• The isomorphism of categories $[\mathcal C, \mathcal C]^\mathrm{op} \cong [\mathcal C^\mathrm{op}, \mathcal C^\mathrm{op}]$ preserves identity functors
• Opposite bifunctor
• Opposite monoidal category

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]

you were right, inverse-unique does give very elegant solutions here. thank you! i just have some style considerations.

[Lavenza]

Pull request preview

New pages

• Cat.Monoidal.Opposite (+88, -0)
• Cat.Instances.Product.Duality (+57, -0)
• Cat.Functor.Bifunctor.Duality (+53, -0)

Changed pages

• Cat.Instances.Functor.Duality (+9, -0)
• Cat.Instances.Product (+0, -1)

[jajaperson]

oh hang on I picked up a typo let me fix that

[jajaperson]

also I think the imports can be cleaned up a bit, on that now

[ncfavier]

perhaps we should have some reflection helpers for these trivial category isos, à la Cat.Functor.Naturality.Reflection