Definition same_fiber_eqrel {X Y : hSet} (f : X → Y) : eqrel X. Proof. use make_eqrel. - intros x y. exact ((f x) = (f y)). - use iseqrelconstr. + intros ? ? ? xy yz; exact (xy @ yz). + intro; reflexivity. + intros ? ? eq; exact (!eq). Defined.