Deduce 0-groupoid universal properties from GraphQuotient

[gio256]

In #1900 and #2106, we consider the (funext-free) 0-groupoid universal property of the coequalizer. We should prove a similar universal property for GraphQuotient and investigate whether we can use this to deduce 0-groupoid universal properties for other colimits as well as the related results in Colimits/CoeqUnivProp.v.

See also #1259 and Homotopy/Suspension, which provided the template for the work on coequalizers.