{B A} (f g : B -> A) {P} (h : Coeq f g -> P) : {k : A -> P & k o f == k o g}. Proof. exists (h o coeq). intros b. exact (ap h (cglue b)). Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod. Require Import Colimits.GraphQuotient.