(P : GraphQuotient R -> Type@{k}) (gq' : forall a, P (gq a)) (gqglue' : forall a b (s : R a b), gqglue s # gq' a = gq' b) : forall x, P x := fun x => match x with | gq a => fun _ => gq' a end gqglue'.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Equivalences. Require Import Types.Universe Types.Paths Types.Arrow Types.Sigma Cubical.DPath.