feat(hott/types): a bit of cleanup

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

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)
+  definition fiber_eq {x y : fiber f b} (p : point x = point y)
-    : x = y :=
+    (q : point_eq x = ap f p ⬝ point_eq y) : x = y :=
   to_inv !equiv_fiber_eq ⟨p, q⟩
 
 end fiber

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)
+  definition pi_transport_constant {C : A → A' → Type} (p : a = a') (f : Π(b : A'), C a b) (b : A')
-    : Π(b : A'), (transport (λa, Π(b : A'), C a b) p f) b = transport (λa, C a b) p (f b) :=
+    : (transport (λa, Π(b : A'), C a b) p f) b = transport (λa, C a b) p (f b) :=
-  eq.rec_on p (λx, idp)
+  eq.rec_on p idp
 
   /- Maps on paths -/
 

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,