{A B : Type} (f f' : A -> B) {R : A -> A -> Type} {S : B -> B -> Type} (e : forall a b, R a b -> S (f a) (f b)) (e' : forall a b, R a b -> S (f' a) (f' b)) (p : f == f') (q : forall a b r, transport011 S (p a) (p b) (e a b r) = e' a b r) : functor_gq f e == functor_gq f' e'. Proof. snrapply GraphQuotient_ind. - simpl; intro. apply ap. apply p. - intros a b s. nrapply (transport_paths_FlFr' (gqglue s)). rhs nrefine (1 @@ _). 2: apply GraphQuotient_rec_beta_gqglue. lhs nrefine (_ @@ 1). 1: apply GraphQuotient_rec_beta_gqglue. apply moveL_Mp. symmetry. destruct (q a b s). lhs nrapply (ap_transport011 _ _ (fun s _ => gqglue)). rhs nrapply concat_p_pp. nrapply transport011_paths. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Equivalences. Require Import Types.Universe Types.Paths Types.Arrow Types.Sigma Cubical.DPath.