From c50db9899d904f46bf28c114f4be5610a6a99e9e Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Thu, 6 Nov 2014 00:14:58 -0500
Subject: [PATCH] feat(library/hott) add thm: to give a section of a fibration
 it suffices to provide it for the image of an equivalence

---
 library/hott/equiv.lean | 22 +++++++++++++++++++++-
 1 file changed, 21 insertions(+), 1 deletion(-)

diff --git a/library/hott/equiv.lean b/library/hott/equiv.lean
index d07a57949..4877147af 100644
--- a/library/hott/equiv.lean
+++ b/library/hott/equiv.lean
@@ -193,7 +193,6 @@ namespace IsEquiv
 
   --Rewrite rules
   section
-  variables (Hf : IsEquiv f)
 
   definition moveR_M (Hf : IsEquiv f) {x : A} {y : B} (p : x ≈ (inv f) y) : (f x ≈ y) :=
     (ap f p) ⬝ (retr f y)
@@ -226,6 +225,27 @@ namespace IsEquiv
         ⬝ whiskerR !concat_Vp _
         ⬝ !concat_1p)
 
+  -- The function equiv_rect says that given an equivalence f : A → B,
+  -- and a hypothesis from B, one may always assume that the hypothesis
+  -- is in the image of e.
+
+  -- In fibrational terms, if we have a fibration over B which has a section
+  -- once pulled back along an equivalence f : A → B, then it has a section
+  -- over all of B.
+
+  definition equiv_rect (Hf : IsEquiv f) (P : B -> Type) :
+      (Πx, P (f x)) → (Πy, P y) :=
+    (λg y, path.transport _ (retr f y) (g (f⁻¹ y)))
+
+  definition equiv_rect_comp (Hf : IsEquiv f) (P : B → Type)
+      (df : Π (x : A), P (f x)) (x : A) : equiv_rect Hf P df (f x) ≈ df x :=
+    let eq1 := (apD df (sect f x)) in
+    calc equiv_rect Hf P df (f x)
+          ≈ path.transport P (retr f (f x)) (df (f⁻¹ (f x))) : idp
+      ... ≈ path.transport P (ap f (sect f x)) (df (f⁻¹ (f x))) : adj f
+      ... ≈ path.transport (P ∘ f) (sect f x) (df (f⁻¹ (f x))) : transport_compose
+      ... ≈ df x : eq1
+
   end
 
 end IsEquiv