{A : Type} (P : A -> Type) {x y : A} (p : y = x) (u : P x) (v : P y) : transport P p^ u = v <~> u = transport P p v := Build_Equiv _ _ (moveL_transport_p P p u v) _. Global Instance isequiv_moveR_equiv_M `{IsEquiv A B f} (x : A) (y : B) : IsEquiv (@moveR_equiv_M A B f _ x y). Proof. unfold moveR_equiv_M. refine (@isequiv_compose _ _ (ap f) _ _ (fun q => q @ eisretr f y) _). Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics.