{A : Type} (P : A -> Type) {x y : A} (p : y = x) (u : P x) (v : P y) : u = transport P p v <~> transport P p^ u = v := Build_Equiv _ _ (moveR_transport_V P p u v) _. Global Instance isequiv_moveL_transport_V {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) (v : P y) : IsEquiv (moveL_transport_V P p u v). Proof. srapply isequiv_adjointify. - apply moveR_transport_p. - intro q; apply moveL_moveR_transport_p. - intro q; apply moveR_moveL_transport_V. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics.