Categorical duality & writing maintainable code

Stream: mathlib4

[Brendan Seamas Murphy]

I'd like to split the CategoryTheory.MonoidalClosed typeclass into two separate left closed and right closed classes. Since the monoidal opposite of a category C is definitionally equal to C we could in principle define RightClosed X := LeftClosed (mop X), ihom_r X := ihom_l (mop X), etc and milk the def eq for all it's worth. But this seems like a bad idea, and not in harmony with other dualities like limits/colimits. We could also define everything separately but still use the definitional-equality-duality to use the proofs for left closed stuff for right closed stuff. The more principled way of doing this would be to say that every construction on one side is equal to the transport of the construction on the other side along the canonical equivalence C ≈ C^Mop. But this leads to some very complicated theorem statements, and I'm not sure mathlib even has certain constructions we'd need for this (eg conjugating an adjunction by an equivalence). I know additive vs multiplicative notation has a similar duplication issue and solves it with annotations/macros, could something like that work here?

I'd like to hear any thoughts people have on this, especially about how the design choices in other parts of the the category theory library came to be what they are. I would like to not fall victim to combinatorial explosion if possible!

[Brendan Seamas Murphy]

(I'm also uncertain why some things are structures and some are defintions. What makes the opposite category more different from the original category than the monoidal opposite is?)

[Eric Wieser]

(I'd suggest renaming this thread to include "category theory" for visibility, since I think the design space there is rather different to many other parts of mathlib)

[Joël Riou]

Brendan Seamas Murphy said:

(I'm also uncertain why some things are structures and some are defintions. What makes the opposite category more different from the original category than the monoidal opposite is?)

See https://github.com/leanprover-community/mathlib4/pull/3193 for the reason why the opposite category is a structure.

[Brendan Seamas Murphy]

The same issue in your original post exists for MonoidalOpposite, should it be changed too? (this is a genuine question, I have no issue with the fact that Opposite is a structure)

[Kim Morrison]

Yes, I think it should be changed.

[Brendan Seamas Murphy]

Atm the hom types of the monoidal opposite are defined via InducedCategory.category. However this still gives us a defeq Hom X Y = Hom (mop X) (mop Y), which I think we're trying to avoid. Should the homs be Hom X Y := (Hom (unmop X) (unmop Y))ᴹᵒᵖ?

[Brendan Seamas Murphy]

(we might want an Inducing property on functors like for topological spaces?)

[Brendan Seamas Murphy]

To see what I mean by avoiding combinatorial explosion, take a look at the simp lemmas added in commit ac0ae4d in the file Mathlib/CategoryTheory/Monoidal/Opposite.lean