Definition homothfiber1 {X Y : UU} (f g : X -> Y) (h : f ~ g) (y : Y) (xe : hfiber f y) : hfiber g y. Proof. intros. set (x := pr1 xe). set (e := pr2 xe). apply (make_hfiber g x (!(h x) @ e)). Defined.