forall (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) (a b: A) (s : R a b), apD (GraphQuotient_ind P gq' gqglue') (gqglue s) = gqglue' a b s.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Equivalences. Require Import Types.Universe Types.Paths Types.Arrow Types.Sigma Cubical.DPath.