`{IsEquiv A B f} (x : A) (y : B) : (x = f^-1 y) <~> (f x = y) := Build_Equiv _ _ (@moveR_equiv_M A B f _ x y) _. Global Instance isequiv_moveR_equiv_V `{IsEquiv A B f} (x : B) (y : A) : IsEquiv (@moveR_equiv_V A B f _ x y). Proof. unfold moveR_equiv_V. refine (@isequiv_compose _ _ (ap f^-1) _ _ (fun q => q @ eissect f y) _). Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics.