diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean
index a77beda18..8bed0f0d6 100644
--- a/hott/types/sigma.hlean
+++ b/hott/types/sigma.hlean
@@ -244,6 +244,10 @@ namespace sigma
     : (Σa, B a) ≃ Σa, B' a :=
   sigma_equiv_sigma equiv.refl Hg
 
+  definition sigma_equiv_sigma_left [constructor] (Hf : A ≃ A') :
+      (Σa, B a) ≃ (Σa', B (to_inv Hf a')) :=
+  sigma_equiv_sigma Hf (λ a, equiv_ap B !right_inv⁻¹)
+
   definition ap_sigma_functor_eq_dpair (p : a = a') (q : b =[p] b') :
     ap (sigma_functor f g) (sigma_eq p q) = sigma_eq (ap f p) (pathover.rec_on q idpo) :=
   by induction q; reflexivity