fact: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Equivalences