From 3468ab8a9fa2901b14cac7eec288237823c16a29 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 20 Sep 2018 15:53:05 +0200
Subject: [PATCH] rename nondep to constant

---
 hott/types/fiber.hlean | 10 ++--------
 hott/types/sigma.hlean | 10 +++++-----
 hott/types/univ.hlean  |  2 +-
 3 files changed, 8 insertions(+), 14 deletions(-)

diff --git a/hott/types/fiber.hlean b/hott/types/fiber.hlean
index f6fa70c18..84a500a0f 100644
--- a/hott/types/fiber.hlean
+++ b/hott/types/fiber.hlean
@@ -165,9 +165,7 @@ namespace fiber
   definition fiber_pr1 (B : A → Type) (a : A) : fiber (pr1 : (Σa, B a) → A) a ≃ B a :=
   calc
     fiber pr1 a ≃ Σu, u.1 = a            : fiber.sigma_char
-            ... ≃ Σa' (b : B a'), a' = a : sigma_assoc_equiv
-            ... ≃ Σa' (p : a' = a), B a' : sigma_equiv_sigma_right (λa', !comm_equiv_nondep)
-            ... ≃ Σu, B u.1              : sigma_assoc_equiv
+            ... ≃ Σu, B u.1              : sigma_assoc_comm_equiv
             ... ≃ B a                    : sigma_equiv_of_is_contr_left _ _
 
   definition sigma_fiber_equiv (f : A → B) : (Σb, fiber f b) ≃ A :=
@@ -266,12 +264,8 @@ namespace fiber
               apply sigma_equiv_sigma_right, 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
+            : sigma_sigma_eq_left
       ... ≃ Σ(p : P a), f a p = q
             :
             begin
diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean
index 73d8e82f5..f9c8b4263 100644
--- a/hott/types/sigma.hlean
+++ b/hott/types/sigma.hlean
@@ -218,13 +218,13 @@ namespace sigma
   by induction p; induction bc; reflexivity
 
   /- The special case when the second variable doesn't depend on the first is simpler. -/
-  definition sigma_transport_nondep {B : Type} {C : A → B → Type} (p : a = a')
+  definition sigma_transport_constant {B : Type} {C : A → B → Type} (p : a = a')
     (bc : Σ(b : B), C a b) : p ▸ bc = ⟨bc.1, p ▸ bc.2⟩ :=
   by induction p; induction bc; reflexivity
 
   /- Or if the second variable contains a first component that doesn't depend on the first. -/
 
-  definition sigma_transport2_nondep {C : A → Type} {D : Π a:A, B a → C a → Type} (p : a = a')
+  definition sigma_transport2_constant {C : A → Type} {D : Π a:A, B a → C a → Type} (p : a = a')
       (bcd : Σ(b : B a) (c : C a), D a b c) : p ▸ bcd = ⟨p ▸ bcd.1, p ▸ bcd.2.1, p ▸D2 bcd.2.2⟩ :=
   begin
     induction p, induction bcd with b cd, induction cd, reflexivity
@@ -250,7 +250,7 @@ namespace sigma
     induction s using idp_rec_on, apply idpo
   end
 
-  definition sigma_pathover_nondep {B : Type} {C : A → B → Type} (p : a = a')
+  definition sigma_pathover_constant {B : Type} {C : A → B → Type} (p : a = a')
     (u : Σ(b : B), C a b) (v : Σ(b : B), C a' b)
     (r : u.1 = v.1) (s : pathover (λx, C (prod.pr1 x) (prod.pr2 x)) u.2 (prod.prod_eq p r) v.2) : u =[p] v :=
   begin
@@ -462,7 +462,7 @@ namespace sigma
     proof (λp, prod.destruct p (λa b, idp)) qed
     proof (λs, destruct s (λa b, idp)) qed)
 
-  definition comm_equiv_nondep (A B : Type) : (Σ(a : A), B) ≃ Σ(b : B), A :=
+  definition comm_equiv_constant (A B : Type) : (Σ(a : A), B) ≃ Σ(b : B), A :=
   calc
     (Σ(a : A), B) ≃ A × B       : equiv_prod
               ... ≃ B × A       : prod_comm_equiv
@@ -472,7 +472,7 @@ namespace sigma
     : (Σ(v : Σa, B a), C v.1) ≃ (Σ(u : Σa, C a), B u.1) :=
   calc    (Σ(v : Σa, B a), C v.1)
         ≃ (Σa (b : B a), C a)     : sigma_assoc_equiv
-    ... ≃ (Σa (c : C a), B a)     : sigma_equiv_sigma_right (λa, !comm_equiv_nondep)
+    ... ≃ (Σa (c : C a), B a)     : sigma_equiv_sigma_right (λa, !comm_equiv_constant)
     ... ≃ (Σ(u : Σa, C a), B u.1) : sigma_assoc_equiv
 
   /- Interaction with other type constructors -/
diff --git a/hott/types/univ.hlean b/hott/types/univ.hlean
index 4db075a89..1e48c8d59 100644
--- a/hott/types/univ.hlean
+++ b/hott/types/univ.hlean
@@ -115,7 +115,7 @@ namespace univ
                                                    (λb, !sigma_assoc_equiv)
       ... ≃ Σb X (x : X), X = fiber f b        : sigma_equiv_sigma_right
                                                    (λb, sigma_equiv_sigma_right
-                                                   (λX, !comm_equiv_nondep))
+                                                   (λX, !comm_equiv_constant))
       ... ≃ Σb (v : ΣX, X), v.1 = fiber f b    : sigma_equiv_sigma_right
                                                    (λb, !sigma_assoc_equiv⁻¹ᵉ)
       ... ≃ Σb (Y : Type*), Y = fiber f b      : sigma_equiv_sigma_right