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