quotient_ind_prop' : forall P : quotient R -> Type, forall (Hprop' : forall x, IsHProp (P (class_of _ x))), (forall x, P (class_of _ x)) -> forall y, P y. Proof. intros ? ? dclass. apply quotient_ind with dclass. - simple refine (quotient_ind R (fun x => IsHSet (P x)) _ _); cbn beta; try exact _. intros; apply path_ishprop. - intros. apply path_ishprop. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Truncations.Core.