fact: Definition hrel_set (X : hSet) : hSet := make_hSet (hrel X) (isaset_hrel X).
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions