Quotient_rec@{i j k l} {A : Type@{i}} (R : Relation@{i j} A) (P : Type@{l}) `{IsHSet P} (pclass : A -> P) (peq : forall a b, R a b -> pclass a = pclass b) : Quotient@{i j k} R -> P. Proof. srapply Trunc_rec; snrapply GraphQuotient_rec. - exact pclass. - exact peq. Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import TruncType. Require Import Colimits.GraphQuotient. Require Import Truncations.Core.