`{Funext} {B A f g} {P : @Coeq B A f g -> Type} (h : forall w : Coeq f g, P w) : h = Coeq_ind P (h o coeq) (fun b => apD h (cglue b)) := path_forall _ _ (Coeq_ind_eta_homotopic h).
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod. Require Import Colimits.GraphQuotient.