type synonym or one field structure?

Stream: mathlib4

[Kevin Buzzard]

If X^new is "X but with a different typeclass", then what governs whether we use a type synonym or a one-field structure when defining it?
Examples:

def OrderDual (α : Type*) : Type _ :=
  α

(changing <= to >=) is a type synonym, but

structure PreOpposite (α : Type u) : Type u where
  /-- The element of `PreOpposite α` that represents `x : α`. -/ op' ::
  /-- The element of `α` represented by `x : PreOpposite α`. -/ unop' : α

def MulOpposite (α : Type u) : Type u :=
  PreOpposite α

(changing a * b to b * a) is a one field structure.

[Jireh Loreaux]

I think the answer is: "do we want to abuse defeq?" If so, then we use the former. If not, then the latter. But I could be wrong.

[Eric Wieser]

I think the answer is a pragmatic one: we had performance issues during the port and MulOpposite fell into our firing line

[Eric Wieser]

Both of these are good examples of types where a synonym is more useful than a one-field structure, as in both cases it's reasonable to want a "very" canonical identification between F (F X) and X

[Jireh Loreaux]

Well, throughout the order library we're always doing lemma Antitone.... := Monotone.... (α := αᵒᵈ)

[Eric Wieser]

For types like Set, I think we could switch to a one-field structure, because we almost never abuse defeq (except for in analysis somewhere where we didn't like the notation...)

[Eric Wieser]

A good example of the case where a one-field structure would be a good idea is AddMonoidAlgebra; there's no use in any type defeq. Unfortunately, the tradeoff is between:

• Having lots of ways to shoot yourself in the foot
• Having to write a very large amount of boilerplate

[Eric Wieser]

See #7932 for an example of what writing that boilerplate looks like