{B A f g} (P : @Coeq B A f g -> Type) `{forall x, IsHProp (P x)} (i : forall a, P (coeq a)) : forall x, P x. Proof. snrapply Coeq_ind. 1: exact i. intros b. rapply path_ishprop. Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod. Require Import Colimits.GraphQuotient.