fix(tests): fix tests to reflect recent changes

tests/lean/531.hlean

@@ -35,30 +35,30 @@ namespace colimit
 
   /-protected-/ constant rec : Π [D : diagram] {P : colimit D → Type}
     (Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x))
-    (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x)
+    (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▸ Pincl (hom j x) = Pincl x)
       (y : colimit D), P y
 
   -- {P : my_colim f → Type} (Hinc : Π⦃n : ℕ⦄ (a : A n), P (inc f a))
-  -- (Heq : Π(n : ℕ) (a : A n), inc_eq f a ▹ Hinc (f a) = Hinc a) : Πaa, P aa
+  -- (Heq : Π(n : ℕ) (a : A n), inc_eq f a ▸ Hinc (f a) = Hinc a) : Πaa, P aa
   -- init_hit
 
   definition comp_incl [D : diagram] {P : colimit D → Type}
     (Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x))
-    (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x)
+    (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▸ Pincl (hom j x) = Pincl x)
       {i : Iob} (x : ob i) : rec Pincl Pglue (ι x) = Pincl x :=
   sorry --idp
 
   --set_option pp.notation false
   definition comp_cglue [D : diagram] {P : colimit D → Type}
     (Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x))
-    (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x)
+    (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▸ Pincl (hom j x) = Pincl x)
       {j : Ihom} (x : ob (dom j)) : apd (rec Pincl Pglue) (cglue j x) = sorry ⬝ Pglue j x ⬝ sorry :=
   --the sorry's in the statement can be removed when comp_incl is definitional
   sorry --idp
 
   protected definition rec_on [D : diagram] {P : colimit D → Type} (y : colimit D)
     (Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x))
-    (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x) : P y :=
+    (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▸ Pincl (hom j x) = Pincl x) : P y :=
   colimit.rec Pincl Pglue y
 
 end colimit
@@ -115,18 +115,18 @@ parameters {TL BL TR : Type.{u}} (f : TL → BL) (g : TL → TR)
   protected theorem rec {P : pushout → Type} --make def
     (Pinl : Π(x : BL), P (inl x))
     (Pinr : Π(x : TR), P (inr x))
-    (Pglue : Π(x : TL), glue x ▹ Pinl (f x) = Pinr (g x))
+    (Pglue : Π(x : TL), glue x ▸ Pinl (f x) = Pinr (g x))
       (y : pushout) : P y :=
   begin
     fapply (@colimit.rec_on _ _ y),
     { intros [i, x], cases i,
-       exact (coherence x ▹ Pinl (f x)),
+       exact (coherence x ▸ Pinl (f x)),
        apply Pinl,
        apply Pinr},
     { intros [j, x], cases j,
         exact idp,
       esimp [pushout_ob.cases_on],
-      apply concat, rotate 1, apply (idpath (coherence x ▹ Pinl (f x))),
+      apply concat, rotate 1, apply (idpath (coherence x ▸ Pinl (f x))),
       apply concat, apply (ap (transport _ _)), apply (idpath (Pinr (g x))),
       apply eq_tr_of_inv_tr_eq,
       rewrite -{(transport (λ (x : pushout), P x) (inverse (coherence x)) (transport P (@cglue _ tt x) (Pinr (g x))))}con_tr,

tests/lean/hott/329.hlean

@@ -3,16 +3,16 @@ open eq sigma
 variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type}
           {a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {u v w : Σa, B a}
 
-definition path_sigma_dpair (p : a = a') (q : p ▹ b = b') : sigma.mk a b = sigma.mk a' b' :=
+definition path_sigma_dpair (p : a = a') (q : p ▸ b = b') : sigma.mk a b = sigma.mk a' b' :=
 eq.rec_on p (λb b' q, eq.rec_on q idp) b b' q
 
-definition path_sigma (p :  pr1 u = pr1 v) (q : p ▹ pr2 u = pr2 v) : u = v :=
+definition path_sigma (p :  pr1 u = pr1 v) (q : p ▸ pr2 u = pr2 v) : u = v :=
 destruct u
          (λu1 u2, destruct v (λ v1 v2, path_sigma_dpair))
          p q
 
-definition path_path_sigma_lemma' {p1 : a = a'} {p2 : p1 ▹ b = b'} {q2 : p1 ▹ b = b'}
+definition path_path_sigma_lemma' {p1 : a = a'} {p2 : p1 ▸ b = b'} {q2 : p1 ▸ b = b'}
-    (s : idp ▹ p2 = q2) : path_sigma p1 p2 = path_sigma p1 q2 :=
+    (s : idp ▸ p2 = q2) : path_sigma p1 p2 = path_sigma p1 q2 :=
 begin
   apply (eq.rec_on s),
   apply idp,

tests/lean/hott/433.hlean

@@ -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],
@@ -77,23 +77,23 @@ namespace pi
      (Π(b : B a), transportD B C p b (f b) = g (eq.transport B p b)) ≃
      (eq.transport (λa, Π(b : B a), C a b) p f = g) -/
   definition dpath_pi (H : funext) (p : a = a') (f : Π(b : B a), C a b) (g : Π(b' : B a'), C a' b')
-    : (Π(b : B a), p ▹D (f b) = g (p ▹ b)) ≃ (p ▹ f = g) :=
+    : (Π(b : B a), p ▸D (f b) = g (p ▸ b)) ≃ (p ▸ f = g) :=
   eq.rec_on p (λg, homotopy_equiv_path H f g) g
 
   section open sigma sigma.ops
   /- more implicit arguments:
-  (Π(b : B a), eq.transport C (sigma.path p idp) (f b) = g (p ▹ b)) ≃
+  (Π(b : B a), eq.transport C (sigma.path p idp) (f b) = g (p ▸ b)) ≃
   (Π(b : B a), transportD B (λ(a : A) (b : B a), C ⟨a, b⟩) p b (f b) = g (eq.transport B p b)) -/
   definition dpath_pi_sigma {C : (Σa, B a) → Type} (p : a = a')
     (f : Π(b : B a), C ⟨a, b⟩) (g : Π(b' : B a'), C ⟨a', b'⟩) :
-    (Π(b : B a), (sigma.sigma_eq p idp) ▹ (f b) = g (p ▹ b)) ≃ (Π(b : B a), p ▹D (f b) = g (p ▹ b)) :=
+    (Π(b : B a), (sigma.sigma_eq p idp) ▸ (f b) = g (p ▸ b)) ≃ (Π(b : B a), p ▸D (f b) = g (p ▸ b)) :=
   eq.rec_on p (λg, !equiv.refl) g
   end
 
   variables (f0 : A' → A) (f1 : Π(a':A'), B (f0 a') → B' a')
 
   definition transport_V [reducible] (P : A → Type) {x y : A} (p : x = y) (u : P y) : P x :=
-  p⁻¹ ▹ u
+  p⁻¹ ▸ u
 
   protected definition functor_pi : (Π(a:A), B a) → (Π(a':A'), B' a') := (λg a', f1 a' (g (f0 a')))
   /- Equivalences -/
@@ -114,7 +114,7 @@ namespace pi
   apply apd,
   intro h, beta,
   apply eq_of_homotopy, intro a, esimp,
-  apply (transport_V (λx, right_inv f0 a ▹ x = h a) (left_inv (f1 _) _)),
+  apply (transport_V (λx, right_inv f0 a ▸ x = h a) (left_inv (f1 _) _)),
   esimp [function.id],
   apply apd
   end

tests/lean/hott/443.hlean

@@ -1,6 +1,6 @@
 import algebra.group algebra.category
 
-open eq sigma unit category path_algebra
+open eq sigma unit category algebra
 
 section
   parameters {P₀ : Type} [P : precategory P₀]

tests/lean/hott/443_b.hlean

@@ -1,6 +1,6 @@
 import algebra.group algebra.category
 
-open eq sigma unit category path_algebra equiv
+open eq sigma unit category algebra equiv
 
 set_option pp.implicit true
 set_option pp.universes true

tests/lean/hott/457.hlean

@@ -1,6 +1,6 @@
 import algebra.group
 
-open eq path_algebra
+open eq algebra
 
 definition foo {A : Type} (a b c : A) (H₁ : a = c) (H₂ : c = b)  : a = b :=
 begin

tests/lean/hott/531b.hlean

@@ -35,30 +35,30 @@ namespace colimit
 
   /-protected-/ constant rec : Π [D : diagram] {P : colimit D → Type}
     (Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x))
-    (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x)
+    (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▸ Pincl (hom j x) = Pincl x)
       (y : colimit D), P y
 
   -- {P : my_colim f → Type} (Hinc : Π⦃n : ℕ⦄ (a : A n), P (inc f a))
-  -- (Heq : Π(n : ℕ) (a : A n), inc_eq f a ▹ Hinc (f a) = Hinc a) : Πaa, P aa
+  -- (Heq : Π(n : ℕ) (a : A n), inc_eq f a ▸ Hinc (f a) = Hinc a) : Πaa, P aa
   -- init_hit
 
   definition comp_incl [D : diagram] {P : colimit D → Type}
     (Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x))
-    (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x)
+    (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▸ Pincl (hom j x) = Pincl x)
       {i : Iob} (x : ob i) : rec Pincl Pglue (ι x) = Pincl x :=
   sorry --idp
 
   --set_option pp.notation false
   definition comp_cglue [D : diagram] {P : colimit D → Type}
     (Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x))
-    (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x)
+    (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▸ Pincl (hom j x) = Pincl x)
       {j : Ihom} (x : ob (dom j)) : apd (rec Pincl Pglue) (cglue j x) = sorry ⬝ Pglue j x ⬝ sorry :=
   --the sorry's in the statement can be removed when comp_incl is definitional
   sorry --idp
 
   protected definition rec_on [D : diagram] {P : colimit D → Type} (y : colimit D)
     (Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x))
-    (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x) : P y :=
+    (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▸ Pincl (hom j x) = Pincl x) : P y :=
   colimit.rec Pincl Pglue y
 
 end colimit
@@ -119,20 +119,20 @@ parameters {TL BL TR : Type.{u}} (f : TL → BL) (g : TL → TR)
   protected theorem rec {P : pushout → Type} --make def
     (Pinl : Π(x : BL), P (inl x))
     (Pinr : Π(x : TR), P (inr x))
-    (Pglue : Π(x : TL), glue x ▹ Pinl (f x) = Pinr (g x))
+    (Pglue : Π(x : TL), glue x ▸ Pinl (f x) = Pinr (g x))
       (y : pushout) : P y :=
   begin
     fapply (@colimit.rec_on _ _ y),
     { intros [i, x], cases i,
-       exact (coherence x ▹ Pinl (f x)),
+       exact (coherence x ▸ Pinl (f x)),
        apply Pinl,
        apply Pinr},
     { intros [j, x],
       cases j,
       exact idp,
       change (transport P (@cglue _ tt x) (Pinr (g x)) = transport P (coherence x) (Pinl (f x))),
-           --(@cglue _ tt x ▹ (Pinr (g x)) = (coherence x ▹ Pinl (f x))),
+           --(@cglue _ tt x ▸ (Pinr (g x)) = (coherence x ▸ Pinl (f x))),
-      apply concat;rotate 1;apply (idpath (coherence x ▹ Pinl (f x))),
+      apply concat;rotate 1;apply (idpath (coherence x ▸ Pinl (f x))),
       apply concat;apply (ap (transport _ _));apply (idpath (Pinr (g x))),
       apply tr_eq_of_eq_inv_tr,
 --      rewrite -{(transport (λ (x : pushout), P x) (inverse (coherence x)) (transport P (@cglue _ tt x) (Pinr (g x))))}tr_con,

tests/lean/hott/crash1.hlean

@@ -2,7 +2,7 @@ import types.sigma types.prod
 import algebra.binary algebra.group
 open eq eq.ops
 
-namespace path_algebra
+namespace algebra
 
 variable {A : Type}
 
@@ -20,4 +20,4 @@ structure zero_ne_one_class [class] (A : Type) extends has_zero A, has_one A :=
 structure semiring [class] (A : Type) extends add_comm_monoid A, monoid A,
   distrib A, mul_zero_class A, zero_ne_one_class A
 
-end path_algebra
+end algebra

tests/lean/hott/len_eq.hlean

@@ -88,9 +88,9 @@ match n with
   | zero      := take v w He, rfl
   | (succ m₁) :=
     take (v : vector A zero) (w : vector A (succ m₁)),
-    empty.elim _ (ninh (inhabited.mk (head w)))
+    empty.elim (ninh (inhabited.mk (head w)))
   end
 | (succ n₁) :=
   take (v : vector A (succ n₁)) (w : vector A m),
-  empty.elim _ (ninh (inhabited.mk (head v)))
+  empty.elim (ninh (inhabited.mk (head v)))
 end

tests/lean/hott/rewriter1.hlean

@@ -1,5 +1,5 @@
 import algebra.group
-open path_algebra
+open algebra
 
 constant f {A : Type} : A → A → A
 
@@ -7,7 +7,7 @@ theorem test1 {A : Type} [s : add_comm_group A] (a b c : A) : f (a + 0) (f (a +
 begin
   rewrite [
     add_zero at {1, 3}, -- rewrite 1st and 3rd occurrences
-    {0 + _}add_comm]   -- apply commutativity to (0 + _)
+    {0 + _}add.comm]   -- apply commutativity to (0 + _)
 end
 
 axiom Ax {A : Type} [s₁ : has_mul A] [s₂ : has_one A] (a : A) : f (a * 1) (a * 1) = 1