From d1cb0018c042cfea8d186bf4203424f78c3b4c1a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 29 Apr 2015 10:15:13 -0700
Subject: [PATCH] fix(tests): adjust tests to reflect changes in the HoTT
 library

---
 tests/lean/abbrev_paren.hlean          |  2 +-
 tests/lean/hott/433.hlean              | 24 ++++++++++++------------
 tests/lean/hott/443.hlean              |  2 +-
 tests/lean/hott/443_b.hlean            |  2 +-
 tests/lean/hott/bug_struct_level.hlean |  2 +-
 tests/lean/hott/len_eq.hlean           |  2 +-
 tests/lean/hott/rw_eta.hlean           |  7 +++----
 7 files changed, 20 insertions(+), 21 deletions(-)

diff --git a/tests/lean/abbrev_paren.hlean b/tests/lean/abbrev_paren.hlean
index 289bb075a..c615bf8d4 100644
--- a/tests/lean/abbrev_paren.hlean
+++ b/tests/lean/abbrev_paren.hlean
@@ -1,4 +1,4 @@
-import algebra.precategory.basic
+import algebra.category
 
 open category
 
diff --git a/tests/lean/hott/433.hlean b/tests/lean/hott/433.hlean
index 63a2fbfe1..87ee447b9 100644
--- a/tests/lean/hott/433.hlean
+++ b/tests/lean/hott/433.hlean
@@ -24,11 +24,11 @@ namespace pi
 
   /- Now we show how these things compute. -/
 
-  definition apD10_path_pi (H : funext) (h : f ∼ g) : apD10 (eq_of_homotopy h) ∼ h :=
-  apD10 (retr apD10 h)
+  definition apd10_path_pi (H : funext) (h : f ∼ g) : apd10 (eq_of_homotopy h) ∼ h :=
+  apd10 (right_inv apd10 h)
 
-  definition path_pi_eta (H : funext) (p : f = g) : eq_of_homotopy (apD10 p) = p :=
-  sect apD10 p
+  definition path_pi_eta (H : funext) (p : f = g) : eq_of_homotopy (apd10 p) = p :=
+  left_inv apd10 p
 
   print classes
 
@@ -38,11 +38,11 @@ namespace pi
   /- The identification of the path space of a dependent function space, up to equivalence, is of course just funext. -/
 
   definition path_equiv_homotopy (H : funext) (f g : Πx, B x) : (f = g) ≃ (f ∼ g) :=
-  equiv.mk _ !is_equiv_apD
+  equiv.mk _ !is_equiv_apd
 
   definition is_equiv_path_pi [instance] (H : funext) (f g : Πx, B x)
       : is_equiv (@eq_of_homotopy _ _ f g) :=
-  is_equiv_inv apD10
+  is_equiv_inv apd10
 
   definition homotopy_equiv_path (H : funext) (f g : Πx, B x) : (f ∼ g) ≃ (f = g) :=
   equiv.mk _ (is_equiv_path_pi H f g)
@@ -51,7 +51,7 @@ namespace pi
 
   protected definition transport (p : a = a') (f : Π(b : B a), C a b)
     : (transport (λa, Π(b : B a), C a b) p f)
-      ∼ (λb, transport (C a') !tr_inv_tr (transportD _ _ p _ (f (p⁻¹ ▹ b)))) :=
+      ∼ (λb, transport (C a') !tr_inv_tr (transportD _ p _ (f (p⁻¹ ▹ b)))) :=
   eq.rec_on p (λx, idp)
 
   /- A special case of [transport_pi] where the type [B] does not depend on [A],
@@ -102,7 +102,7 @@ namespace pi
       : is_equiv (functor_pi f0 f1) :=
   begin
   apply (adjointify (functor_pi f0 f1) (functor_pi (f0⁻¹)
-        (λ(a : A) (b' : B' (f0⁻¹ a)), transport B (retr f0 a) ((f1 (f0⁻¹ a))⁻¹ b')))),
+        (λ(a : A) (b' : B' (f0⁻¹ a)), transport B (right_inv f0 a) ((f1 (f0⁻¹ a))⁻¹ b')))),
   intro h, apply eq_of_homotopy,
   esimp [functor_pi, function.compose], -- simplify (and unfold function_pi and function.compose)
   --first subgoal
@@ -110,13 +110,13 @@ namespace pi
   rewrite adj,
   rewrite -transport_compose,
   rewrite {f1 a' _}(fn_tr_eq_tr_fn _ f1 _),
-  rewrite (retr (f1 _) _),
-  apply apD,
+  rewrite (right_inv (f1 _) _),
+  apply apd,
   intro h, beta,
   apply eq_of_homotopy, intro a, esimp,
-  apply (transport_V (λx, retr f0 a ▹ x = h a) (sect (f1 _) _)),
+  apply (transport_V (λx, right_inv f0 a ▹ x = h a) (left_inv (f1 _) _)),
   esimp [function.id],
-  apply apD
+  apply apd
   end
 
 end pi
diff --git a/tests/lean/hott/443.hlean b/tests/lean/hott/443.hlean
index 8ad62b67c..b8db96081 100644
--- a/tests/lean/hott/443.hlean
+++ b/tests/lean/hott/443.hlean
@@ -1,4 +1,4 @@
-import algebra.group algebra.precategory.basic
+import algebra.group algebra.category
 
 open eq sigma unit category path_algebra
 
diff --git a/tests/lean/hott/443_b.hlean b/tests/lean/hott/443_b.hlean
index d78102bde..224c48723 100644
--- a/tests/lean/hott/443_b.hlean
+++ b/tests/lean/hott/443_b.hlean
@@ -1,4 +1,4 @@
-import algebra.groupoid algebra.group
+import algebra.group algebra.category
 
 open eq sigma unit category path_algebra equiv
 
diff --git a/tests/lean/hott/bug_struct_level.hlean b/tests/lean/hott/bug_struct_level.hlean
index 3cf440d69..5328258ca 100644
--- a/tests/lean/hott/bug_struct_level.hlean
+++ b/tests/lean/hott/bug_struct_level.hlean
@@ -1,4 +1,4 @@
-import algebra.precategory.basic
+import algebra.category
 
 open category
 
diff --git a/tests/lean/hott/len_eq.hlean b/tests/lean/hott/len_eq.hlean
index 65c32ac31..60b399f6f 100644
--- a/tests/lean/hott/len_eq.hlean
+++ b/tests/lean/hott/len_eq.hlean
@@ -1,4 +1,4 @@
-import init.axioms.ua
+import init.ua
 open nat unit equiv is_trunc
 
 inductive vector (A : Type) : nat → Type :=
diff --git a/tests/lean/hott/rw_eta.hlean b/tests/lean/hott/rw_eta.hlean
index 152b85fb5..bac3a8027 100644
--- a/tests/lean/hott/rw_eta.hlean
+++ b/tests/lean/hott/rw_eta.hlean
@@ -17,8 +17,7 @@ definition eq_of_homotopy2 {f g : Πa b, C a b} (H : f ∼2 g) : f = g :=
 eq_of_homotopy (λa, eq_of_homotopy (H a))
 
 definition apD100 {f g : Πa b, C a b} (p : f = g) : f ∼2 g :=
-λa b, apD10 (apD10 p a) b
-
+λa b, apd10 (apd10 p a) b
 
 local attribute eq_of_homotopy [reducible]
 
@@ -26,8 +25,8 @@ definition foo (f g : Πa b, C a b) (H : f ∼2 g) (a : A)
   : apD100 (eq_of_homotopy2 H) a = H a :=
 begin
   esimp [apD100, eq_of_homotopy2, eq_of_homotopy],
-  rewrite (retr apD10 (λ(a : A), eq_of_homotopy (H a))),
-  apply (retr apD10)
+  rewrite (right_inv apd10 (λ(a : A), eq_of_homotopy (H a))),
+  apply (right_inv apd10)
 end
 
 end hide