Corollary isaset_hfiber {X Y : UU} (f : X -> Y) (y : Y) : isaset X -> isaset Y -> isaset (hfiber f y). Proof. intros isX isY. apply isaset_total2. assumption. intro. apply isasetaprop. apply isY. Defined.