fact: Definition Coeq_unrec {B A} (f g : B -> A) {P} (h : Coeq f g -> P) : {k : A -> P & k o f == k o g}.
imports: Basics Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod Cubical.DPath Colimits.GraphQuotient