Corollary weqhfibertocontr {X Y : UU} (f : X -> Y) (y : Y) (is : iscontr Y) : weq (hfiber f y) X. Proof. intros. split with (hfiberpr1 f y). apply (isofhlevelfhfiberpr1 0 f y (hlevelntosn 0 _ is)). Defined.