Quiver.opposite

Stream: maths

[Calle Sönne]

This is how Quiver.opposite is defined in mathlib:

/-- `Vᵒᵖ` reverses the direction of all arrows of `V`. -/
instance opposite {V} [Quiver V] : Quiver Vᵒᵖ :=
  ⟨fun a b => (unop b ⟶ unop a)ᵒᵖ⟩

Why is there an ᵒᵖ also at the level of morphisms? Why not just define them as unop b ⟶ unop a? I'm guessing this is to avoid some kind of ambiguity between unop b ⟶ unop a and aᵒᵖ ⟶ bᵒᵖ, but I don't see where exactly this might become an issue.

[Joël Riou]

I made the change because it was too permissive, see https://github.com/leanprover-community/mathlib4/pull/3193

[Calle Sönne]

Joël Riou said:

I made the change because it was too permissive, see https://github.com/leanprover-community/mathlib4/pull/3193

thanks!