`{Funext} {B A} (f g : B -> A) P : {h : A -> P & h o f == h o g} <~> (Coeq f g -> P) := Build_Equiv _ _ _ (isequiv_Coeq_rec f g P).
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod. Require Import Colimits.GraphQuotient.