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