{A B C : Type} (f : A -> B) (g : B -> C) {R : A -> A -> Type} {S : B -> B -> Type} {T : C -> C -> Type} (e : forall a b, R a b -> S (f a) (f b)) (e' : forall a b, S a b -> T (g a) (g b)) : functor_gq g e' o (functor_gq f e) == functor_gq (g o f) (fun a b r => e' _ _ (e _ _ r)). Proof. snrapply GraphQuotient_ind. 1: reflexivity. intros a b s. nrapply (transport_paths_FlFr' (gqglue s)). apply equiv_p1_1q. lhs nrapply (ap_compose (functor_gq f e) (functor_gq g e') (gqglue s)). lhs nrapply ap. 1: apply GraphQuotient_rec_beta_gqglue. lhs nrapply GraphQuotient_rec_beta_gqglue. exact (GraphQuotient_rec_beta_gqglue _ _ _ _ s)^. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Equivalences. Require Import Types.Universe Types.Paths Types.Arrow Types.Sigma Cubical.DPath.