Quotient_ind@{i j k l} {A : Type@{i}} (R : Relation@{i j} A) (P : Quotient@{i j k} R -> Type@{l}) {sP : forall x, IsHSet (P x)} (pclass : forall a, P (class_of R a)) (peq : forall a b (H : R a b), qglue H # pclass a = pclass b) : forall x, P x. Proof. rapply Trunc_ind; srapply GraphQuotient_ind. - exact pclass. - intros a b p. lhs nrapply (transport_compose P). exact (peq a b p). Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import TruncType. Require Import Colimits.GraphQuotient. Require Import Truncations.Core.