Definition homothfiberretr {X Y : UU} (f g : X -> Y) (h : f ~ g) (y : Y) (xe : hfiber g y) : homothfiber1 f g h y (homothfiber2 f g h y xe) = xe. Proof. intros. induction xe as [x e]. simpl. fold (make_hfiber g x e). set (xe1 := make_hfiber g x (! h x @ h x @ e)). set (xe2 := make_hfiber g x e). apply (hfibertriangle2 g xe1 xe2 (idpath _)). simpl. assert (ee : ∏ a b c : Y, ∏ p : a = b, ∏ q : b = c, !p @ (p @ q) = q). { intros. induction p. induction q. apply idpath. } apply ee. Defined.