feat(hott): prove HoTT book Theorem 4.7.7

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)
 

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}

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⟩