Definition homotinvweqweq0 {X Y : UU} (w : X ≃ Y) : ∏ x : X, x = invmap w (w x). Proof. intros. unfold invmap. set (xe1 := weqccontrhfiber w (w x)). set (xe2 := make_hfiber w x (idpath (w x))). set (p := weqccontrhfiber2 w (w x) xe2). apply (maponpaths pr1 p). Defined.