Definition switch_weq' {X Y} (f:X ≃ Y) {x y} : invweq f y = x -> y = f x. Proof. intros p. exact (! homotweqinvweq f y @ maponpaths f p). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.PartA.