From 2c2250108443cabb3fb86b1100f51ca252e1be7b Mon Sep 17 00:00:00 2001
From: Ulrik Buchholtz <ulrikbuchholtz@gmail.com>
Date: Sat, 26 Sep 2015 18:01:33 -0400
Subject: [PATCH] feat(hott): prove HoTT book Theorem 4.7.6

---
 hott/init/trunc.hlean  |  4 ++++
 hott/types/fiber.hlean | 45 ++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 49 insertions(+)

diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean
index c9450d4c1f..d13c684af0 100644
--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@@ -199,6 +199,10 @@ namespace is_trunc
     : is_contr (Σ(x : A), a = x) :=
   is_contr.mk (sigma.mk a idp) (λp, sigma.rec_on p (λ b q, eq.rec_on q idp))
 
+  definition is_contr_sigma_eq' [instance] [priority 800] {A : Type} (a : A)
+    : is_contr (Σ(x : A), x = a) :=
+  is_contr.mk (sigma.mk a idp) (λp, sigma.rec_on p (λ b q, eq.rec_on q idp))
+
   definition is_contr_unit : is_contr unit :=
   is_contr.mk star (λp, unit.rec_on p idp)
 
diff --git a/hott/types/fiber.hlean b/hott/types/fiber.hlean
index 3ae3efdcdf..93da442af2 100644
--- a/hott/types/fiber.hlean
+++ b/hott/types/fiber.hlean
@@ -44,3 +44,48 @@ namespace fiber
   to_inv !fiber_eq_equiv ⟨p, q⟩
 
 end fiber
+
+open function is_equiv is_trunc
+
+namespace fiber
+  /- Theorem 4.7.6 -/
+  variables {A : Type} {P Q : A → Type}
+
+  /- 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)
+    : fiber (sigma_functor id f) ⟨a , q⟩ ≃ fiber (f a) q :=
+  calc
+    fiber (sigma_functor id f) ⟨a , q⟩
+          ≃ Σ(w : Σx, P x), ⟨w.1 , f w.1 w.2 ⟩ = ⟨a , q⟩
+            : sigma_char
+      ... ≃ Σ(x : A), Σ(p : P x), ⟨x , f x p⟩ = ⟨a , q⟩
+            : sigma_assoc_equiv
+      ... ≃ Σ(x : A), Σ(p : P x), Σ(H : x = a), f x p =[H] q
+            :
+            begin
+              apply sigma_equiv_sigma_id, intro x,
+              apply sigma_equiv_sigma_id, intro p,
+              apply sigma_eq_equiv
+            end
+      ... ≃ Σ(x : A), Σ(H : x = a), Σ(p : P x), f x p =[H] q
+            :
+            begin
+              apply sigma_equiv_sigma_id, intro x,
+              apply sigma_comm_equiv
+            end
+      ... ≃ Σ(w : Σx, x = a), Σ(p : P w.1), f w.1 p =[w.2] q
+            : sigma_assoc_equiv
+      ... ≃ Σ(p : P (center (Σx, x=a)).1), f (center (Σx, x=a)).1 p =[(center (Σx, x=a)).2] q
+            : sigma_equiv_of_is_contr_left
+      ... ≃ Σ(p : P a), f a p =[idpath a] q
+            : equiv_of_eq idp
+      ... ≃ Σ(p : P a), f a p = q
+            :
+            begin
+              apply sigma_equiv_sigma_id, intro p,
+              apply pathover_idp
+            end
+      ... ≃ fiber (f a) q
+            : sigma_char
+
+end fiber