From a79a3043ed04f5df2ee268131234dd6bd7f294b1 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Sun, 19 Apr 2015 15:58:13 -0400
Subject: [PATCH] feat(hott/types): a bit of cleanup

---
 hott/types/equiv.hlean | 2 +-
 hott/types/fiber.hlean | 8 ++++----
 hott/types/pi.hlean    | 6 +++---
 hott/types/sigma.hlean | 2 +-
 4 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean
index 8b049fd57..5c850e995 100644
--- a/hott/types/equiv.hlean
+++ b/hott/types/equiv.hlean
@@ -22,7 +22,7 @@ namespace is_equiv
     definition is_contr_fiber_of_is_equiv (b : B) : is_contr (fiber f b) :=
     is_contr.mk
       (fiber.mk (f⁻¹ b) (retr f b))
-      (λz, fiber.rec_on z (λa p, fiber.eq_mk ((ap f⁻¹ p)⁻¹ ⬝ sect f a) (calc
+      (λz, fiber.rec_on z (λa p, fiber_eq ((ap f⁻¹ p)⁻¹ ⬝ sect f a) (calc
         retr f b = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ((ap (f ∘ f⁻¹) p) ⬝ retr f b) : by rewrite inv_con_cancel_left
              ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (retr f (f a) ⬝ p)       : by rewrite ap_con_eq_con
              ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (ap f (sect f a) ⬝ p)    : by rewrite adj
diff --git a/hott/types/fiber.hlean b/hott/types/fiber.hlean
index 0658f0ae5..7f3572a14 100644
--- a/hott/types/fiber.hlean
+++ b/hott/types/fiber.hlean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2014 Floris van Doorn. All rights reserved.
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Module: types.fiber
@@ -9,7 +9,7 @@ Ported from Coq HoTT
 Theorems about fibers
 -/
 
-import types.sigma types.eq
+import .sigma .eq
 
 structure fiber {A B : Type} (f : A → B) (b : B) :=
   (point : A)
@@ -44,8 +44,8 @@ namespace fiber
     {apply (ap (λx, x = _)), rewrite transport_eq_Fl}
   end
 
-  definition eq_mk {x y : fiber f b} (p : point x = point y) (q : point_eq x = ap f p ⬝ point_eq y)
-    : x = y :=
+  definition fiber_eq {x y : fiber f b} (p : point x = point y)
+    (q : point_eq x = ap f p ⬝ point_eq y) : x = y :=
   to_inv !equiv_fiber_eq ⟨p, q⟩
 
 end fiber
diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean
index 3d69832e0..040d60f4e 100644
--- a/hott/types/pi.hlean
+++ b/hott/types/pi.hlean
@@ -57,9 +57,9 @@ namespace pi
 
   /- A special case of [transport_pi] where the type [B] does not depend on [A],
       and so it is just a fixed type [B]. -/
-  definition pi_transport_constant {C : A → A' → Type} (p : a = a') (f : Π(b : A'), C a b)
-    : Π(b : A'), (transport (λa, Π(b : A'), C a b) p f) b = transport (λa, C a b) p (f b) :=
-  eq.rec_on p (λx, idp)
+  definition pi_transport_constant {C : A → A' → Type} (p : a = a') (f : Π(b : A'), C a b) (b : A')
+    : (transport (λa, Π(b : A'), C a b) p f) b = transport (λa, C a b) p (f b) :=
+  eq.rec_on p idp
 
   /- Maps on paths -/
 
diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean
index 09d49d47e..a516a9d47 100644
--- a/hott/types/sigma.hlean
+++ b/hott/types/sigma.hlean
@@ -200,7 +200,7 @@ namespace sigma
     -- "rewrite retr (g (f⁻¹ a'))"
     apply concat, apply (ap (λx, (transport B' (retr f a') x))), apply (retr (g (f⁻¹ a'))),
     show retr f a' ▹ ((retr f a')⁻¹ ▹ b') = b',
-    from tr_inv_tr B' (retr f a') b'
+    from tr_inv_tr _ (retr f a') b'
   end
   begin
     intro u,