{A : Type} (R : Relation A) (B : Type) `{IsHSet B} (dclass : A -> A -> B) (dequiv_l : forall a a' b, R a a' -> dclass a b = dclass a' b) (dequiv_r : forall a b b', R b b' -> dclass a b = dclass a b') : A / R -> A / R -> B. Proof. srapply Quotient_ind2. - exact dclass. - intros; lhs nrapply transport_const. by apply dequiv_l. - intros; lhs nrapply transport_const. by apply dequiv_r. Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import TruncType. Require Import Colimits.GraphQuotient. Require Import Truncations.Core.