@Coeq B A f g <~> @Coeq B' A' f' g' := Build_Equiv _ _ (functor_coeq h k p q) _.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod. Require Import Colimits.GraphQuotient.