{A R P} (c : A -> P) (g : forall a b, R a b -> c a = c b) : GraphQuotient R -> P. Proof. srapply GraphQuotient_ind. 1: exact c. intros a b s. refine (transport_const _ _ @ g a b s). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Equivalences. Require Import Types.Universe Types.Paths Types.Arrow Types.Sigma Cubical.DPath.