From 25ed9d6e5ad861cefb9cfe02b48ed244baed0cd0 Mon Sep 17 00:00:00 2001
From: Ulrik Buchholtz <ulrikbuchholtz@gmail.com>
Date: Sat, 26 Sep 2015 20:23:39 -0400
Subject: [PATCH] feat(hott): prove HoTT book Theorem 4.7.7

---
 hott/book.md           |  2 +-
 hott/types/equiv.hlean | 25 +++++++++++++++++++++++++
 hott/types/fiber.hlean |  3 ++-
 3 files changed, 28 insertions(+), 2 deletions(-)

diff --git a/hott/book.md b/hott/book.md
index 895a04fb86..c70043409b 100644
--- a/hott/book.md
+++ b/hott/book.md
@@ -90,7 +90,7 @@ Chapter 4: Equivalences
 - 4.4 (Contractible fibers): [types.equiv](types/equiv.hlean)
 - 4.5 (On the definition of equivalences): no formalizable content
 - 4.6 (Surjections and embeddings): [function](function.hlean)
-- 4.7 (Closure properties of equivalences): Theorem 4.7.6 in [types.fiber](types/fiber.hlean) (the rest not formalized)
+- 4.7 (Closure properties of equivalences): Theorem 4.7.6 in [types.fiber](types/fiber.hlean), Theorem 4.7.7 in [types.equiv](types/equiv.hlean)
 - 4.8 (The object classifier): not formalized
 - 4.9 (Univalence implies function extensionality): [init.funext](init/funext.hlean)
 
diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean
index cbbb870707..56ce1551ef 100644
--- a/hott/types/equiv.hlean
+++ b/hott/types/equiv.hlean
@@ -104,6 +104,31 @@ namespace is_equiv
 
 end is_equiv
 
+namespace is_equiv
+
+  /- Theorem 4.7.7 -/
+  variables {A : Type} {P Q : A → Type}
+  variable (f : Πa, P a → Q a)
+
+  definition is_fiberwise_equiv [class] := Πa, is_equiv (f a)
+
+  definition is_equiv_total_of_is_fiberwise_equiv [H : is_fiberwise_equiv f] : is_equiv (sigma_functor id f) :=
+  begin
+    apply is_equiv_of_is_contr_fun, apply sigma.rec, intros a q,
+    apply @is_contr_equiv_closed _ _ (fiber_total_equiv f q)⁻¹ᵉ,
+    apply @is_contr_fun_of_is_equiv _ _ (f a),
+    exact H a
+  end
+
+  definition is_fiberwise_equiv_of_is_equiv_total [H : is_equiv (sigma_functor id f)] : is_fiberwise_equiv f :=
+  begin
+    intro a,
+    apply is_equiv_of_is_contr_fun, intro q,
+    apply @is_contr_equiv_closed _ _ (fiber_total_equiv f q)
+  end
+
+end is_equiv
+
 namespace equiv
   open is_equiv
   variables {A B C : Type}
diff --git a/hott/types/fiber.hlean b/hott/types/fiber.hlean
index 6ca26a312a..ad102ed2b1 100644
--- a/hott/types/fiber.hlean
+++ b/hott/types/fiber.hlean
@@ -66,9 +66,10 @@ open function is_equiv
 namespace fiber
   /- Theorem 4.7.6 -/
   variables {A : Type} {P Q : A → Type}
+  variable (f : Πa, P a → Q a)
 
   /- Note that the map on total spaces/sigmas is just sigma_functor id -/
-  definition fiber_total_equiv (f : Πa, P a → Q a) {a : A} (q : Q a)
+  definition fiber_total_equiv {a : A} (q : Q a)
     : fiber (sigma_functor id f) ⟨a , q⟩ ≃ fiber (f a) q :=
   calc
     fiber (sigma_functor id f) ⟨a , q⟩