(P : (@quotient sR) -> Type) {sP : forall x, IsHSet (P x)} (dclass : forall x, P (class_of x)) (dequiv : (forall x y (H : R x y), (related_classes_eq H) # (dclass x) = dclass y)) : forall q, P q := fun q => match q with class_of a => fun _ _ => dclass a end sP dequiv.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Truncations.Core.