equiv_functor_coeq' {B A f g B' A' f' g'} (h : B <~> B') (k : A <~> A') (p : k o f == f' o h) (q : k o g == g' o h) : @Coeq B A f g <~> @Coeq B' A' f' g' := 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.