Definition homotweqinvweqweq {X Y : UU} (w : X ≃ Y) (x : X) : maponpaths w (homotinvweqweq w x) = homotweqinvweq w (w x). Proof. intros. unfold homotinvweqweq. unfold homotinvweqweq0. set (hfid := make_hfiber w x (idpath (w x))). set (hfcc := weqccontrhfiber w (w x)). unfold homotweqinvweq. apply diaglemma2. apply (@hfibertriangle1 _ _ w _ hfid hfcc (weqccontrhfiber2 w (w x) hfid)). Defined.