Definition homotinvweqweq' {X} {P:X->Type} (irr:∏ x (p q:P x), p = q) (s:∏ x, P x) (w:total2 P) : invmap (weqpr1_irr_sec irr s) (weqpr1_irr_sec irr s w) = w. Proof. revert w; intros [x p]. apply pair_path_in2. apply irr. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Equivalences.