Digraph vs Quiver.{0}

Stream: mathlib4

[Oliver Nash]

Mathlib contains both docs#Quiver (with a moderate API) and docs#Digraph (with a small API) but mathematically Quiver.{0} is the same as Digraph.

So we could do any of:

1. Continue with both, living with the duplication
2. Make Digraph an abbrev for Quiver.{0} (and write some custom API for this case)
3. Something else

Has anyone thought about this?

[Shreyas Srinivas]

(deleted)

[Robin Arnez]

I guess Quiver being a class vs Digraph being a structure might be a relevant discrepancy?

[Kim Morrison]

(Noting also that Category extends CategoryStruct which extends Quiver. I don't know whether "un-classing" Quiver would cause a problem there.)