{A : Type} {R : Relation A} {B : Type} {S : Relation B} {C : Type} {T : Relation C} (f : A -> B) (fresp : forall a b, R a b -> S (f a) (f b)) (g : B -> C) (gresp : forall a b, S a b -> T (g a) (g b)) : Quotient_functor R T (g o f) (fun a b => (gresp _ _) o (fresp a b)) == Quotient_functor S T g gresp o Quotient_functor R S f fresp. Proof. by srapply Quotient_ind_hprop. Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import TruncType. Require Import Colimits.GraphQuotient. Require Import Truncations.Core.