`{Funext} : Coeq f g <~> Coequalizer f g. Proof. srapply colimit_unicity. 3: eapply iscoequalizer_Coeq. eapply iscolimit_colimit. Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.ParallelPair. Require Import Diagrams.Cocone. Require Import Colimits.Colimit. Require Import Colimits.Coeq.