Lemma iscontrhfiberl2 {X Y : UU} (f g : X -> Y) (h : f ~ g) (y : Y) (is : iscontr (hfiber f y)) : iscontr (hfiber g y). Proof. intros. set (a := homothfiber1 f g h y). set (b := homothfiber2 f g h y). set (eab := homothfiberretr f g h y). apply (iscontrretract a b eab is). Defined.