{A : Type} (R : Relation A) (P : A / R -> A / R -> Type) `{forall x y, IsHSet (P x y)} (dclass : forall a b, P (class_of R a) (class_of R b)) (dequiv_l : forall a a' b (p : R a a'), transport (fun x => P x _) (qglue p) (dclass a b) = dclass a' b) (dequiv_r : forall a b b' (p : R b b'), qglue p # dclass a b = dclass a b') : forall x y, P x y. Proof. intro x. srapply Quotient_ind. - intro b. revert x. srapply Quotient_ind. + intro a. exact (dclass a b). + cbn beta. intros a a' p. by apply dequiv_l. - cbn beta. intros b b' p. revert x. srapply Quotient_ind_hprop; simpl. intro a; 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.