{A R P} (c : A -> P) (g : forall a b, R a b -> c a = c b) (a b : A) (s : R a b) : ap (GraphQuotient_rec c g) (gqglue s) = g a b s. Proof. unfold GraphQuotient_rec. refine (cancelL _ _ _ _ ). refine ((apD_const _ _)^ @ _). rapply GraphQuotient_ind_beta_gqglue. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Equivalences. Require Import Types.Universe Types.Paths Types.Arrow Types.Sigma Cubical.DPath.