Coeq f g -> Type := Coeq_rec Type F (fun x => path_universe (e x)). Local R (a b : A) := {x : B & (f x = a) * (g x = b)}. Local e' (a b : A) : R a b -> (F a <~> F b). Proof. intros [x [[] []]]; exact (e x). Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod. Require Import Colimits.GraphQuotient.