From 377755e5ab0de956c22a5e85cc210a2cfe89f364 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Mon, 30 Nov 2015 19:25:22 -0500
Subject: [PATCH] feat(types/sigma): add lemma

---
 hott/types/sigma.hlean | 4 ++++
 1 file changed, 4 insertions(+)

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