Why unop?

Stream: mathlib4

[Nathaniel Virgo]

Hi, this is my first post. I'm a Lean newbie. I'm hoping to use it for category theory eventually, so I'm trying to familiarise myself with the relevant parts of MathLib while also learning the language.

One question I have is, in MathLib.Data.Opposite and the various places it's imported, why do we have separate op and unop operations, instead of having op be an involution?

Naïvely, I would have expected the opposite of a quiver to be defined something like

def my_op {V} (X : Quiver V) : Quiver V :=
  ⟨ fun a b => b ⟶ a ⟩

so that $(X^\text{op})^\text{op} = X$,

variable (V : Type)
variable (X : Quiver V)
theorem op_op_eq : my_op (my_op X) = X := rfl

This can probably be carried over to categories straightforwardly.

I assume there are good reasons not to do it that way, but I'd like to understand what they are, so that I can get a better feeling for how to work with opposite categories in practice.

[Joël Riou]

Doing so was making too easy to write mathematically meaningless definitions or statements because of abuse of definitional equalities. The trend in the category theory library is to use one-field structures in order to prevent this from happening.

[Edward van de Meent]

In lean, the phrase "let $C$ be a category, and let $X \xrightarrow{f} Y$ be a morphism in $C$" corresponds to the lean code of {C : Type u} [Category.{v} C] {X Y : C} (f : X ⟶ Y). in order to figure out what X ⟶ Y means, lean needs to figure out what instance of Quiver to use here. It does that by looking at the type of X and Y (which is C), and then looking for an instance of Quiver for that type, which it finds via Category.toQuiver. If there are multiple instances of Quiver C lean will behave unpredictable and sometimes choose one, sometimes choose the other, and this in general leads to a bad user experience.
In short, having multiple instances of Quiver for the same type is bad.

If we were to have such a notion of op, in order to state this equality, we would need* op (op X) : C. However, this is only possible if the type of op is* C -> C, so we would also need to define an instance of the opposite category structure on C, which we have decided leads to too much confusion. As Joël said, in the category theory library this was mitigated by making the type Opposite C distinct from C at even the strongest reducibility, using one-field structures. Now, the statement that op is (categorically) an involution is captured by CategoryTheory.opOpEquivalence

*: there is in lean the notion of "reducibility" and "irreducibility" meaning that for certain declarations, lean sometimes doesn't unfold the definition. one can make use of this in order to define Opposite C := C, and define the opposite category on Opposite C rather than C itself, and so long as you make sure to give your variables the correct type, this works... However it turns out that if you don't consistently insert coercions either way to help lean realize if you're working with Opposite C or C, you again get the same issue where lean is confused about what category you're working with.