diff --git a/hott/algebra/category/adjoint.hlean b/hott/algebra/category/adjoint.hlean
index 82d957913..c99eb33c9 100644
--- a/hott/algebra/category/adjoint.hlean
+++ b/hott/algebra/category/adjoint.hlean
@@ -133,7 +133,7 @@ namespace category
 
   definition is_isomorphism_equiv1 (F : C ⇒ D) : is_equivalence F
     ≃ Σ(G : D ⇒ C) (η : functor.id = G ∘f F) (ε : F ∘f G = functor.id),
-        sorry ▹ ap (λ(H : C ⇒ C), F ∘f H) η = ap (λ(H : D ⇒ D), H ∘f F) ε⁻¹ :=
+        sorry ▸ ap (λ(H : C ⇒ C), F ∘f H) η = ap (λ(H : D ⇒ D), H ∘f F) ε⁻¹ :=
   sorry
 
   definition is_isomorphism_equiv2 (F : C ⇒ D) : is_equivalence F
diff --git a/hott/algebra/category/constructions/hset.hlean b/hott/algebra/category/constructions/hset.hlean
index 9af0ee12d..69cebfb56 100644
--- a/hott/algebra/category/constructions/hset.hlean
+++ b/hott/algebra/category/constructions/hset.hlean
@@ -82,7 +82,7 @@ namespace category
           (@is_equiv_subtype_eq_inv _ _ _ _ _))
         !univalence)
       !is_equiv_iso_of_equiv,
-    (iso_of_eq_eq_compose A B)⁻¹ ▹ H
+    (iso_of_eq_eq_compose A B)⁻¹ ▸ H
   end set
 
   definition category_hset [reducible] [instance] : category hset :=
diff --git a/hott/algebra/category/functor.hlean b/hott/algebra/category/functor.hlean
index 27e3d57de..a70f3099e 100644
--- a/hott/algebra/category/functor.hlean
+++ b/hott/algebra/category/functor.hlean
@@ -48,7 +48,7 @@ namespace functor
 
   definition functor_mk_eq' {F₁ F₂ : C → D} {H₁ : Π(a b : C), hom a b → hom (F₁ a) (F₁ b)}
     {H₂ : Π(a b : C), hom a b → hom (F₂ a) (F₂ b)} (id₁ id₂ comp₁ comp₂)
-    (pF : F₁ = F₂) (pH : pF ▹ H₁ = H₂)
+    (pF : F₁ = F₂) (pH : pF ▸ H₁ = H₂)
       : functor.mk F₁ H₁ id₁ comp₁ = functor.mk F₂ H₂ id₂ comp₂ :=
   apd01111 functor.mk pF pH !is_hprop.elim !is_hprop.elim
 
@@ -193,7 +193,7 @@ namespace functor
   end
 
   -- definition ap010_functor_eq' {F₁ F₂ : C ⇒ D} (p : to_fun_ob F₁ = to_fun_ob F₂)
-  --   (q : p ▹ F₁ = F₂) (c : C) :
+  --   (q : p ▸ F₁ = F₂) (c : C) :
   --   ap to_fun_ob (functor_eq (apd10 p) (λa b f, _)) = p := sorry
   -- begin
   --   cases F₂, revert q, apply (homotopy.rec_on p), clear p, esimp, intros p q,
diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean
index b717f7095..b7511708e 100644
--- a/hott/algebra/category/iso.hlean
+++ b/hott/algebra/category/iso.hlean
@@ -77,7 +77,7 @@ namespace iso
 
   definition is_iso_of_split_epi_of_split_mono (f : a ⟶ b) [Hl : split_mono f] [Hr : split_epi f]
     : is_iso f :=
-  is_iso.mk ((retraction_eq_section f) ▹ (retraction_comp f)) (comp_section f)
+  is_iso.mk ((retraction_eq_section f) ▸ (retraction_comp f)) (comp_section f)
 
   definition inverse_unique (H H' : is_iso f) : @inverse _ _ _ _ f H = @inverse _ _ _ _ f H' :=
   inverse_eq_left !left_inverse
@@ -199,13 +199,13 @@ namespace iso
     open funext
     variables {X : Type} {x y : X} {F G : X → ob}
     definition transport_hom_of_eq (p : F = G) (f : hom (F x) (F y))
-      : p ▹ f = hom_of_eq (apd10 p y) ∘ f ∘ inv_of_eq (apd10 p x) :=
+      : p ▸ f = hom_of_eq (apd10 p y) ∘ f ∘ inv_of_eq (apd10 p x) :=
     eq.rec_on p !id_leftright⁻¹
 
     definition transport_hom (p : F ∼ G) (f : hom (F x) (F y))
-      : eq_of_homotopy p ▹ f = hom_of_eq (p y) ∘ f ∘ inv_of_eq (p x) :=
+      : eq_of_homotopy p ▸ f = hom_of_eq (p y) ∘ f ∘ inv_of_eq (p x) :=
     calc
-      eq_of_homotopy p ▹ f =
+      eq_of_homotopy p ▸ f =
         hom_of_eq (apd10 (eq_of_homotopy p) y) ∘ f ∘ inv_of_eq (apd10 (eq_of_homotopy p) x)
           : transport_hom_of_eq
         ... = hom_of_eq (p y) ∘ f ∘ inv_of_eq (p x) : {right_inv apd10 p}
@@ -286,13 +286,13 @@ namespace iso
      by rewrite [-assoc, inverse_comp_cancel_left, left_inverse])
 
   definition inverse_comp_inverse_left [H' : is_iso g] : (q⁻¹ ∘ g)⁻¹ = g⁻¹ ∘ q :=
-  inverse_involutive q ▹ comp_inverse q⁻¹ g
+  inverse_involutive q ▸ comp_inverse q⁻¹ g
 
   definition inverse_comp_inverse_right [H' : is_iso f] : (q ∘ f⁻¹)⁻¹ = f ∘ q⁻¹ :=
-  inverse_involutive f ▹ comp_inverse q f⁻¹
+  inverse_involutive f ▸ comp_inverse q f⁻¹
 
   definition inverse_comp_inverse_inverse [H' : is_iso r] : (q⁻¹ ∘ r⁻¹)⁻¹ = r ∘ q :=
-  inverse_involutive r ▹ inverse_comp_inverse_left q r⁻¹
+  inverse_involutive r ▸ inverse_comp_inverse_left q r⁻¹
   end
 
   section
@@ -306,13 +306,13 @@ namespace iso
   variable [Hq : is_iso q] include Hq
 
   definition comp_eq_of_eq_inverse_comp (H : y = q⁻¹ ∘ g) : q ∘ y = g :=
-  H⁻¹ ▹ comp_inverse_cancel_left q g
+  H⁻¹ ▸ comp_inverse_cancel_left q g
   definition comp_eq_of_eq_comp_inverse (H : w = f ∘ q⁻¹) : w ∘ q = f :=
-  H⁻¹ ▹ inverse_comp_cancel_right f q
+  H⁻¹ ▸ inverse_comp_cancel_right f q
   definition inverse_comp_eq_of_eq_comp (H : z = q ∘ p) : q⁻¹ ∘ z = p :=
-  H⁻¹ ▹ inverse_comp_cancel_left q p
+  H⁻¹ ▸ inverse_comp_cancel_left q p
   definition comp_inverse_eq_of_eq_comp (H : x = r ∘ q) : x ∘ q⁻¹ = r :=
-  H⁻¹ ▹ comp_inverse_cancel_right r q
+  H⁻¹ ▸ comp_inverse_cancel_right r q
   definition eq_comp_of_inverse_comp_eq (H : q⁻¹ ∘ g = y) : g = q ∘ y :=
   (comp_eq_of_eq_inverse_comp H⁻¹)⁻¹
   definition eq_comp_of_comp_inverse_eq (H : f ∘ q⁻¹ = w) : f = w ∘ q :=
diff --git a/hott/algebra/category/precategory.hlean b/hott/algebra/category/precategory.hlean
index f16640539..95cea5fd1 100644
--- a/hott/algebra/category/precategory.hlean
+++ b/hott/algebra/category/precategory.hlean
@@ -186,8 +186,8 @@ namespace category
     (id_id1 : Π (a : ob), comp1 !ID1 !ID1 = ID1 a)
     (id_id2 : Π (a : ob), comp2 !ID2 !ID2 = ID2 a)
     (p : hom1 = hom2)
-    (q : p ▹ comp1 = comp2)
-    (r : p ▹ ID1 = ID2) :
+    (q : p ▸ comp1 = comp2)
+    (r : p ▸ ID1 = ID2) :
     precategory.mk' hom1 comp1 ID1 assoc1 assoc1' id_left1 id_right1 id_id1 homH1
     = precategory.mk' hom2 comp2 ID2 assoc2 assoc2' id_left2 id_right2 id_id2 homH2 :=
   begin
@@ -243,7 +243,7 @@ namespace category
 
   definition Precategory_eq (C D : Precategory)
     (p : carrier C = carrier D)
-    (q : p ▹ (Precategory.struct C) = Precategory.struct D) : C = D :=
+    (q : p ▸ (Precategory.struct C) = Precategory.struct D) : C = D :=
   begin
     cases C, cases D,
     cases p, cases q,
diff --git a/hott/algebra/group.hlean b/hott/algebra/group.hlean
index d5cddb2ee..206e99788 100644
--- a/hott/algebra/group.hlean
+++ b/hott/algebra/group.hlean
@@ -183,16 +183,16 @@ section group
   theorem inv_inj {a b : A} (H : a⁻¹ = b⁻¹) : a = b :=
   calc
     a = (a⁻¹)⁻¹ : inv_inv
-      ... = b : inv_eq_of_mul_eq_one (H⁻¹ ▹ (mul_left_inv _))
+      ... = b : inv_eq_of_mul_eq_one (H⁻¹ ▸ (mul_left_inv _))
 
   --theorem inv_eq_inv_iff_eq (a b : A) : a⁻¹ = b⁻¹ ↔ a = b :=
   --iff.intro (assume H, inv_inj H) (assume H, congr_arg _ H)
 
   --theorem inv_eq_one_iff_eq_one (a b : A) : a⁻¹ = 1 ↔ a = 1 :=
-  --inv_one ▹ !inv_eq_inv_iff_eq
+  --inv_one ▸ !inv_eq_inv_iff_eq
 
   theorem eq_inv_imp_eq_inv {a b : A} (H : a = b⁻¹) : b = a⁻¹ :=
-  H⁻¹ ▹ (inv_inv b)⁻¹
+  H⁻¹ ▸ (inv_inv b)⁻¹
 
   --theorem eq_inv_iff_eq_inv (a b : A) : a = b⁻¹ ↔ b = a⁻¹ :=
   --iff.intro !eq_inv_imp_eq_inv !eq_inv_imp_eq_inv
@@ -229,28 +229,28 @@ section group
 
   -- TODO: better names for the next eight theorems? (Also for additive ones.)
   theorem eq_mul_inv_of_mul_eq {a b c : A} (H : a * b = c) : a = c * b⁻¹ :=
-  H ▹ !mul_inv_cancel_right⁻¹
+  H ▸ !mul_inv_cancel_right⁻¹
 
   theorem eq_inv_mul_of_mul_eq {a b c : A} (H : a * b = c) : b = a⁻¹ * c :=
-  H ▹ !inv_mul_cancel_left⁻¹
+  H ▸ !inv_mul_cancel_left⁻¹
 
   theorem inv_mul_eq_of_eq_mul {a b c : A} (H : a = b * c) : b⁻¹ * a = c :=
-  H⁻¹ ▹ !inv_mul_cancel_left
+  H⁻¹ ▸ !inv_mul_cancel_left
 
   theorem mul_inv_eq_of_eq_mul {a b c : A} (H : a = b * c) : a * c⁻¹ = b :=
-  H⁻¹ ▹ !mul_inv_cancel_right
+  H⁻¹ ▸ !mul_inv_cancel_right
 
   theorem eq_mul_of_mul_inv_eq {a b c : A} (H : a * b⁻¹ = c) : a = c * b :=
-  !inv_inv ▹ (eq_mul_inv_of_mul_eq H)
+  !inv_inv ▸ (eq_mul_inv_of_mul_eq H)
 
   theorem eq_mul_of_inv_mul_eq {a b c : A} (H : a⁻¹ * b = c) : b = a * c :=
-  !inv_inv ▹ (eq_inv_mul_of_mul_eq H)
+  !inv_inv ▸ (eq_inv_mul_of_mul_eq H)
 
   theorem mul_eq_of_eq_inv_mul {a b c : A} (H : a = b⁻¹ * c) : b * a = c :=
-  !inv_inv ▹ (inv_mul_eq_of_eq_mul H)
+  !inv_inv ▸ (inv_mul_eq_of_eq_mul H)
 
   theorem mul_eq_of_eq_mul_inv {a b c : A} (H : a = b * c⁻¹) : a * c = b :=
-  !inv_inv ▹ (mul_inv_eq_of_eq_mul H)
+  !inv_inv ▸ (mul_inv_eq_of_eq_mul H)
 
   --theorem mul_eq_iff_eq_inv_mul (a b c : A) : a * b = c ↔ b = a⁻¹ * c :=
   --iff.intro eq_inv_mul_of_mul_eq mul_eq_of_eq_inv_mul
@@ -318,16 +318,16 @@ section add_group
   theorem neg_inj {a b : A} (H : -a = -b) : a = b :=
   calc
     a = -(-a) : neg_neg
-      ... = b : neq_eq_of_add_eq_zero (H⁻¹ ▹ (add_left_inv _))
+      ... = b : neq_eq_of_add_eq_zero (H⁻¹ ▸ (add_left_inv _))
 
   --theorem neg_eq_neg_iff_eq (a b : A) : -a = -b ↔ a = b :=
   --iff.intro (assume H, neg_inj H) (assume H, congr_arg _ H)
 
   --theorem neg_eq_zero_iff_eq_zero (a b : A) : -a = 0 ↔ a = 0 :=
-  --neg_zero ▹ !neg_eq_neg_iff_eq
+  --neg_zero ▸ !neg_eq_neg_iff_eq
 
   theorem eq_neq_of_eq_neg {a b : A} (H : a = -b) : b = -a :=
-  H⁻¹ ▹ (neg_neg b)⁻¹
+  H⁻¹ ▸ (neg_neg b)⁻¹
 
   --theorem eq_neg_iff_eq_neg (a b : A) : a = -b ↔ b = -a :=
   --iff.intro !eq_neq_of_eq_neg !eq_neq_of_eq_neg
@@ -357,28 +357,28 @@ section add_group
         ... = 0 : add_right_inv)
 
   theorem eq_add_neq_of_add_eq {a b c : A} (H : a + b = c) : a = c + -b :=
-  H ▹ !add_neg_cancel_right⁻¹
+  H ▸ !add_neg_cancel_right⁻¹
 
   theorem eq_neg_add_of_add_eq {a b c : A} (H : a + b = c) : b = -a + c :=
-  H ▹ !neg_add_cancel_left⁻¹
+  H ▸ !neg_add_cancel_left⁻¹
 
   theorem neg_add_eq_of_eq_add {a b c : A} (H : a = b + c) : -b + a = c :=
-  H⁻¹ ▹ !neg_add_cancel_left
+  H⁻¹ ▸ !neg_add_cancel_left
 
   theorem add_neg_eq_of_eq_add {a b c : A} (H : a = b + c) : a + -c = b :=
-  H⁻¹ ▹ !add_neg_cancel_right
+  H⁻¹ ▸ !add_neg_cancel_right
 
   theorem eq_add_of_add_neg_eq {a b c : A} (H : a + -b = c) : a = c + b :=
-  !neg_neg ▹ (eq_add_neq_of_add_eq H)
+  !neg_neg ▸ (eq_add_neq_of_add_eq H)
 
   theorem eq_add_of_neg_add_eq {a b c : A} (H : -a + b = c) : b = a + c :=
-  !neg_neg ▹ (eq_neg_add_of_add_eq H)
+  !neg_neg ▸ (eq_neg_add_of_add_eq H)
 
   theorem add_eq_of_eq_neg_add {a b c : A} (H : a = -b + c) : b + a = c :=
-  !neg_neg ▹ (neg_add_eq_of_eq_add H)
+  !neg_neg ▸ (neg_add_eq_of_eq_add H)
 
   theorem add_eq_of_eq_add_neg {a b c : A} (H : a = b + -c) : a + c = b :=
-  !neg_neg ▹ (add_neg_eq_of_eq_add H)
+  !neg_neg ▸ (add_neg_eq_of_eq_add H)
 
   --theorem add_eq_iff_eq_neg_add (a b c : A) : a + b = c ↔ b = -a + c :=
   --iff.intro eq_neg_add_of_add_eq add_eq_of_eq_neg_add
@@ -426,13 +426,13 @@ section add_group
       ... = b : zero_add
 
   --theorem eq_iff_minus_eq_zero (a b : A) : a = b ↔ a - b = 0 :=
-  --iff.intro (assume H, H ▹ !sub_self) (assume H, eq_of_sub_eq_zero H)
+  --iff.intro (assume H, H ▸ !sub_self) (assume H, eq_of_sub_eq_zero H)
 
   theorem zero_sub (a : A) : 0 - a = -a := !zero_add
 
-  theorem sub_zero (a : A) : a - 0 = a := neg_zero⁻¹ ▹ !add_zero
+  theorem sub_zero (a : A) : a - 0 = a := neg_zero⁻¹ ▸ !add_zero
 
-  theorem sub_neg_eq_add (a b : A) : a - (-b) = a + b := !neg_neg ▹ idp
+  theorem sub_neg_eq_add (a b : A) : a - (-b) = a + b := !neg_neg ▸ idp
 
   theorem neg_sub (a b : A) : -(a - b) = b - a :=
   neq_eq_of_add_eq_zero
@@ -457,7 +457,7 @@ section add_group
   --theorem minus_eq_minus_iff {a b c d : A} (H : a - b = c - d) : a = b ↔ c = d :=
   --calc
   --  a = b ↔ a - b = 0 : eq_iff_minus_eq_zero
-  --    ... ↔ c - d = 0 : H ▹ !iff.refl
+  --    ... ↔ c - d = 0 : H ▸ !iff.refl
   --    ... ↔ c = d : iff.symm (eq_iff_minus_eq_zero c d)
 
 end add_group
@@ -470,11 +470,11 @@ variable [s : add_comm_group A]
 include s
 
   theorem sub_add_eq_sub_sub (a b c : A) : a - (b + c) = a - b - c :=
-  !add_comm ▹ !sub_add_eq_sub_sub_swap
+  !add_comm ▸ !sub_add_eq_sub_sub_swap
 
   theorem neq_add_eq_sub (a b : A) : -a + b = b - a := !add_comm
 
-  theorem neg_add_distrib (a b : A) : -(a + b) = -a + -b := !add_comm ▹ !neq_add_rev
+  theorem neg_add_distrib (a b : A) : -(a + b) = -a + -b := !add_comm ▸ !neq_add_rev
 
   theorem sub_add_eq_add_sub (a b c : A) : a - b + c = a + c - b := !add_right_comm
 
diff --git a/hott/arity.hlean b/hott/arity.hlean
index be15a8fcb..67d2cc5ca 100644
--- a/hott/arity.hlean
+++ b/hott/arity.hlean
@@ -79,23 +79,23 @@ namespace eq
   definition ap01000 (f : X → Πa b c, D a b c) (Hx : x = x') : f x ∼3 f x' :=
   by intros; cases Hx; reflexivity
 
-  definition apd011 (f : Πa, B a → Z) (Ha : a = a') (Hb : (Ha ▹ b) = b')
+  definition apd011 (f : Πa, B a → Z) (Ha : a = a') (Hb : (Ha ▸ b) = b')
       : f a b = f a' b' :=
   by cases Ha; cases Hb; reflexivity
 
-  definition apd0111 (f : Πa b, C a b → Z) (Ha : a = a') (Hb : (Ha ▹ b) = b')
-    (Hc : apd011 C Ha Hb ▹ c = c')
+  definition apd0111 (f : Πa b, C a b → Z) (Ha : a = a') (Hb : (Ha ▸ b) = b')
+    (Hc : apd011 C Ha Hb ▸ c = c')
       : f a b c = f a' b' c' :=
   by cases Ha; cases Hb; cases Hc; reflexivity
 
-  definition apd01111 (f : Πa b c, D a b c → Z) (Ha : a = a') (Hb : (Ha ▹ b) = b')
-    (Hc : apd011 C Ha Hb ▹ c = c') (Hd : apd0111 D Ha Hb Hc ▹ d = d')
+  definition apd01111 (f : Πa b c, D a b c → Z) (Ha : a = a') (Hb : (Ha ▸ b) = b')
+    (Hc : apd011 C Ha Hb ▸ c = c') (Hd : apd0111 D Ha Hb Hc ▸ d = d')
       : f a b c d = f a' b' c' d' :=
   by cases Ha; cases Hb; cases Hc; cases Hd; reflexivity
 
-  definition apd011111 (f : Πa b c d, E a b c d → Z) (Ha : a = a') (Hb : (Ha ▹ b) = b')
-    (Hc : apd011 C Ha Hb ▹ c = c') (Hd : apd0111 D Ha Hb Hc ▹ d = d')
-    (He : apd01111 E Ha Hb Hc Hd ▹ e = e')
+  definition apd011111 (f : Πa b c d, E a b c d → Z) (Ha : a = a') (Hb : (Ha ▸ b) = b')
+    (Hc : apd011 C Ha Hb ▸ c = c') (Hd : apd0111 D Ha Hb Hc ▸ d = d')
+    (He : apd01111 E Ha Hb Hc Hd ▸ e = e')
     : f a b c d e = f a' b' c' d' e' :=
   by cases Ha; cases Hb; cases Hc; cases Hd; cases He; reflexivity
 
@@ -180,11 +180,11 @@ namespace eq
   local attribute funext.is_equiv_apd100 [instance]
   protected definition homotopy2.rec_on {f g : Πa b, C a b} {P : (f ∼2 g) → Type}
     (p : f ∼2 g) (H : Π(q : f = g), P (apd100 q)) : P p :=
-  right_inv apd100 p ▹ H (eq_of_homotopy2 p)
+  right_inv apd100 p ▸ H (eq_of_homotopy2 p)
 
   protected definition homotopy3.rec_on {f g : Πa b c, D a b c} {P : (f ∼3 g) → Type}
     (p : f ∼3 g) (H : Π(q : f = g), P (apd1000 q)) : P p :=
-  right_inv apd1000 p ▹ H (eq_of_homotopy3 p)
+  right_inv apd1000 p ▸ H (eq_of_homotopy3 p)
 
   definition apd10_ap (f : X → Πa, B a) (p : x = x')
     : apd10 (ap f p) = ap010 f p :=
diff --git a/hott/cubical/pathover.hlean b/hott/cubical/pathover.hlean
index 810684524..1d0a1e9ca 100644
--- a/hott/cubical/pathover.hlean
+++ b/hott/cubical/pathover.hlean
@@ -29,20 +29,20 @@ namespace cubical
   pathover.idpatho b
 
   /- equivalences with equality using transport -/
-  definition pathover_of_transport_eq (r : p ▹ b = b₂) : b =[p] b₂ :=
+  definition pathover_of_transport_eq (r : p ▸ b = b₂) : b =[p] b₂ :=
   by cases p; cases r; exact idpo
 
-  definition pathover_of_eq_transport (r : b = p⁻¹ ▹ b₂) : b =[p] b₂ :=
+  definition pathover_of_eq_transport (r : b = p⁻¹ ▸ b₂) : b =[p] b₂ :=
   by cases p; cases r; exact idpo
 
-  definition transport_eq_of_pathover (r : b =[p] b₂) : p ▹ b = b₂ :=
+  definition transport_eq_of_pathover (r : b =[p] b₂) : p ▸ b = b₂ :=
   by cases r; exact idp
 
-  definition eq_transport_of_pathover (r : b =[p] b₂) : b = p⁻¹ ▹ b₂ :=
+  definition eq_transport_of_pathover (r : b =[p] b₂) : b = p⁻¹ ▸ b₂ :=
   by cases r; exact idp
 
   definition pathover_equiv_transport_eq (p : a = a₂) (b : B a) (b₂ : B a₂)
-    : (b =[p] b₂) ≃ (p ▹ b = b₂) :=
+    : (b =[p] b₂) ≃ (p ▸ b = b₂) :=
   begin
     fapply equiv.MK,
     { exact transport_eq_of_pathover},
@@ -52,7 +52,7 @@ namespace cubical
   end
 
   definition pathover_equiv_eq_transport (p : a = a₂) (b : B a) (b₂ : B a₂)
-    : (b =[p] b₂) ≃ (b = p⁻¹ ▹ b₂) :=
+    : (b =[p] b₂) ≃ (b = p⁻¹ ▸ b₂) :=
   begin
     fapply equiv.MK,
     { exact eq_transport_of_pathover},
@@ -61,10 +61,10 @@ namespace cubical
     { intro r, cases r, apply idp},
   end
 
-  definition pathover_transport (p : a = a₂) (b : B a) : b =[p] p ▹ b :=
+  definition pathover_transport (p : a = a₂) (b : B a) : b =[p] p ▸ b :=
   pathover_of_transport_eq idp
 
-  definition transport_pathover (p : a = a₂) (b : B a) : p⁻¹ ▹ b =[p] b :=
+  definition transport_pathover (p : a = a₂) (b : B a) : p⁻¹ ▸ b =[p] b :=
   pathover_of_eq_transport idp
 
   definition concato (r : b =[p] b₂) (r₂ : b₂ =[p₂] b₃) : b =[p ⬝ p₂] b₃ :=
@@ -127,7 +127,7 @@ namespace cubical
     {b₂ : B a} (r : b =[idpath a] b₂) (H : P idpo) : P r :=
   have H2 : P (pathover_idp_of_eq (eq_of_pathover_idp r)),
     from eq.rec_on (eq_of_pathover_idp r) H,
-  left_inv !pathover_idp r ▹ H2
+  left_inv !pathover_idp r ▸ H2
 
   --pathover with fibration B' ∘ f
   definition pathover_compose (B' : A' → Type) (f : A → A') (p : a = a₂)
@@ -240,11 +240,11 @@ namespace cubical
     by cases r; apply (idp_rec_on q); exact idpo
 
     definition ap10o {f : Πb, C a b} {g : Πb₂, C a₂ b₂} (r : f =[p] g)
-      {b : B a} : f b =[apD011o C p !pathover_transport] g (p ▹ b) :=
+      {b : B a} : f b =[apD011o C p !pathover_transport] g (p ▸ b) :=
     by cases r; exact idpo
 
     -- definition equiv_pi_pathover' (f : Πb, C a b) (g : Πb₂, C a₂ b₂) :
-    --   (f =[p] g) ≃ (Π(b : B a), f b =[apD011o C p !pathover_transport] g (p ▹ b)) :=
+    --   (f =[p] g) ≃ (Π(b : B a), f b =[apD011o C p !pathover_transport] g (p ▸ b)) :=
     -- begin
     --   fapply equiv.MK,
     --   { exact ap10o},
diff --git a/hott/cubical/square.hlean b/hott/cubical/square.hlean
index 7d632f0c1..977c33075 100644
--- a/hott/cubical/square.hlean
+++ b/hott/cubical/square.hlean
@@ -82,7 +82,7 @@ namespace cubical
       (s : square t idp l r) (H : P ids) : P s :=
   have H2 : P (square_of_eq (eq_of_square s)),
     from eq.rec_on (eq_of_square s : t ⬝ r = l) (by cases r; cases t; exact H),
-  left_inv (to_fun !square_equiv_eq) s ▹ H2
+  left_inv (to_fun !square_equiv_eq) s ▸ H2
 
   definition rec_on_r {a₀₀ : A}
     {P : Π{a₀₂ a₂₁ : A} {t : a₀₀ = a₂₁} {b : a₀₂ = a₂₁} {l : a₀₀ = a₀₂}, square t b l idp → Type}
@@ -91,7 +91,7 @@ namespace cubical
   let p : l ⬝ b = t := (eq_of_square s)⁻¹ in
   have H2 : P (square_of_eq (eq_of_square s)⁻¹⁻¹),
     from @eq.rec_on _ _ (λx p, P (square_of_eq p⁻¹)) _ p (by cases b; cases l; exact H),
-  left_inv (to_fun !square_equiv_eq) s ▹ !inv_inv ▹ H2
+  left_inv (to_fun !square_equiv_eq) s ▸ !inv_inv ▸ H2
 
   definition rec_on_l {a₀₁ : A}
     {P : Π {a₂₀ a₂₂ : A} {t : a₀₁ = a₂₀} {b : a₀₁ = a₂₂} {r : a₂₀ = a₂₂},
@@ -101,7 +101,7 @@ namespace cubical
   let p : t ⬝ r = b := eq_of_square s ⬝ !idp_con in
   have H2 : P (square_of_eq (p ⬝ !idp_con⁻¹)),
     from eq.rec_on p (by cases r; cases t; exact H),
-  left_inv (to_fun !square_equiv_eq) s ▹ !con_inv_cancel_right ▹ H2
+  left_inv (to_fun !square_equiv_eq) s ▸ !con_inv_cancel_right ▸ H2
 
   definition rec_on_t {a₁₀ : A}
     {P : Π {a₀₂ a₂₂ : A} {b : a₀₂ = a₂₂} {l : a₁₀ = a₀₂} {r : a₁₀ = a₂₂}, square idp b l r → Type}
@@ -115,7 +115,7 @@ namespace cubical
   assert H4 : P (square_of_eq (eq_of_square s)),
     from eq.rec_on !inv_inv H3,
   proof
-    left_inv (to_fun !square_equiv_eq) s ▹ H4
+    left_inv (to_fun !square_equiv_eq) s ▸ H4
   qed
 
   definition rec_on_tb {a : A}
@@ -124,7 +124,7 @@ namespace cubical
       (s : square idp idp l r) (H : P ids) : P s :=
   have H2 : P (square_of_eq (eq_of_square s)),
     from eq.rec_on (eq_of_square s : idp ⬝ r = l) (by cases r; exact H),
-  left_inv (to_fun !square_equiv_eq) s ▹ H2
+  left_inv (to_fun !square_equiv_eq) s ▸ H2
 
   --we can also do the other recursors (lr, tl, tr, bl, br, tbl, tbr, tlr, blr), but let's postpone this until they are needed
 
diff --git a/hott/hit/circle.hlean b/hott/hit/circle.hlean
index 0af9c618e..a1a1ecd6d 100644
--- a/hott/hit/circle.hlean
+++ b/hott/hit/circle.hlean
@@ -25,7 +25,7 @@ namespace circle
   definition loop : base = base := seg1 ⬝ seg2⁻¹
 
   definition rec2 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2)
-    (Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb1 = Pb2) (x : circle) : P x :=
+    (Ps1 : seg1 ▸ Pb1 = Pb2) (Ps2 : seg2 ▸ Pb1 = Pb2) (x : circle) : P x :=
   begin
     fapply (suspension.rec_on x),
     { exact Pb1},
@@ -37,16 +37,16 @@ namespace circle
   end
 
   definition rec2_on [reducible] {P : circle → Type} (x : circle) (Pb1 : P base1) (Pb2 : P base2)
-    (Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb1 = Pb2) : P x :=
+    (Ps1 : seg1 ▸ Pb1 = Pb2) (Ps2 : seg2 ▸ Pb1 = Pb2) : P x :=
   circle.rec2 Pb1 Pb2 Ps1 Ps2 x
 
   theorem rec2_seg1 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2)
-    (Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb1 = Pb2)
+    (Ps1 : seg1 ▸ Pb1 = Pb2) (Ps2 : seg2 ▸ Pb1 = Pb2)
       : apd (rec2 Pb1 Pb2 Ps1 Ps2) seg1 = Ps1 :=
   !rec_merid
 
   theorem rec2_seg2 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2)
-    (Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb1 = Pb2)
+    (Ps1 : seg1 ▸ Pb1 = Pb2) (Ps2 : seg2 ▸ Pb1 = Pb2)
       : apd (rec2 Pb1 Pb2 Ps1 Ps2) seg2 = Ps2 :=
   !rec_merid
 
@@ -71,7 +71,7 @@ namespace circle
     rewrite [-apd_eq_tr_constant_con_ap,↑elim2,rec2_seg2],
   end
 
-  protected definition rec {P : circle → Type} (Pbase : P base) (Ploop : loop ▹ Pbase = Pbase)
+  protected definition rec {P : circle → Type} (Pbase : P base) (Ploop : loop ▸ Pbase = Pbase)
     (x : circle) : P x :=
   begin
     fapply (rec2_on x),
@@ -83,18 +83,18 @@ namespace circle
 --rewrite -tr_con, exact Ploop⁻¹
 
   protected definition rec_on [reducible] {P : circle → Type} (x : circle) (Pbase : P base)
-    (Ploop : loop ▹ Pbase = Pbase) : P x :=
+    (Ploop : loop ▸ Pbase = Pbase) : P x :=
   rec Pbase Ploop x
 
   theorem rec_loop_helper {A : Type} (P : A → Type)
-    {x y : A} {p : x = y} {u : P x} {v : P y} (q : u = p⁻¹ ▹ v) :
+    {x y : A} {p : x = y} {u : P x} {v : P y} (q : u = p⁻¹ ▸ v) :
     eq_inv_tr_of_tr_eq (tr_eq_of_eq_inv_tr q) = q :=
   by cases p; exact idp
 
   definition con_refl {A : Type} {x y : A} (p : x = y) : p ⬝ refl _ = p :=
   eq.rec_on p idp
 
-  theorem rec_loop {P : circle → Type} (Pbase : P base) (Ploop : loop ▹ Pbase = Pbase) :
+  theorem rec_loop {P : circle → Type} (Pbase : P base) (Ploop : loop ▸ Pbase = Pbase) :
     apd (rec Pbase Ploop) loop = Ploop :=
   begin
     rewrite [↑loop,apd_con,↑rec,↑rec2_on,↑base,rec2_seg1,apd_inv,rec2_seg2,↑ap], --con_idp should work here
@@ -141,7 +141,7 @@ namespace circle
   definition nonidp (x : circle) : x = x :=
   circle.rec_on x loop
     (calc
-      loop ▹ loop = loop⁻¹ ⬝ loop ⬝ loop : transport_eq_lr
+      loop ▸ loop = loop⁻¹ ⬝ loop ⬝ loop : transport_eq_lr
         ... = loop : by rewrite [con.left_inv, idp_con])
 
   definition nonidp_neq_idp : nonidp ≠ (λx, idp) :=
diff --git a/hott/hit/coeq.hlean b/hott/hit/coeq.hlean
index dbf92bf57..0c06798d3 100644
--- a/hott/hit/coeq.hlean
+++ b/hott/hit/coeq.hlean
@@ -33,7 +33,7 @@ parameters {A B : Type.{u}} (f g : A → B)
   eq_of_rel coeq_rel (Rmk f g x)
 
   protected definition rec {P : coeq → Type} (P_i : Π(x : B), P (coeq_i x))
-    (Pcp : Π(x : A), cp x ▹ P_i (f x) = P_i (g x)) (y : coeq) : P y :=
+    (Pcp : Π(x : A), cp x ▸ P_i (f x) = P_i (g x)) (y : coeq) : P y :=
   begin
     fapply (type_quotient.rec_on y),
     { intro a, apply P_i},
@@ -41,11 +41,11 @@ parameters {A B : Type.{u}} (f g : A → B)
   end
 
   protected definition rec_on [reducible] {P : coeq → Type} (y : coeq)
-    (P_i : Π(x : B), P (coeq_i x)) (Pcp : Π(x : A), cp x ▹ P_i (f x) = P_i (g x)) : P y :=
+    (P_i : Π(x : B), P (coeq_i x)) (Pcp : Π(x : A), cp x ▸ P_i (f x) = P_i (g x)) : P y :=
   rec P_i Pcp y
 
   theorem rec_cp {P : coeq → Type} (P_i : Π(x : B), P (coeq_i x))
-    (Pcp : Π(x : A), cp x ▹ P_i (f x) = P_i (g x))
+    (Pcp : Π(x : A), cp x ▸ P_i (f x) = P_i (g x))
       (x : A) : apd (rec P_i Pcp) (cp x) = Pcp x :=
   !rec_eq_of_rel
 
diff --git a/hott/hit/colimit.hlean b/hott/hit/colimit.hlean
index 4813f96c3..71120d2aa 100644
--- a/hott/hit/colimit.hlean
+++ b/hott/hit/colimit.hlean
@@ -36,7 +36,7 @@ section
 
    protected definition rec {P : colimit → Type}
     (Pincl : Π⦃i : I⦄ (x : A i), P (ι x))
-    (Pglue : Π(j : J) (x : A (dom j)), cglue j x ▹ Pincl (f j x) = Pincl x)
+    (Pglue : Π(j : J) (x : A (dom j)), cglue j x ▸ Pincl (f j x) = Pincl x)
       (y : colimit) : P y :=
   begin
     fapply (type_quotient.rec_on y),
@@ -46,12 +46,12 @@ section
 
   protected definition rec_on [reducible] {P : colimit → Type} (y : colimit)
     (Pincl : Π⦃i : I⦄ (x : A i), P (ι x))
-    (Pglue : Π(j : J) (x : A (dom j)), cglue j x ▹ Pincl (f j x) = Pincl x) : P y :=
+    (Pglue : Π(j : J) (x : A (dom j)), cglue j x ▸ Pincl (f j x) = Pincl x) : P y :=
   rec Pincl Pglue y
 
   theorem rec_cglue {P : colimit → Type}
     (Pincl : Π⦃i : I⦄ (x : A i), P (ι x))
-    (Pglue : Π(j : J) (x : A (dom j)), cglue j x ▹ Pincl (f j x) = Pincl x)
+    (Pglue : Π(j : J) (x : A (dom j)), cglue j x ▸ Pincl (f j x) = Pincl x)
       {j : J} (x : A (dom j)) : apd (rec Pincl Pglue) (cglue j x) = Pglue j x :=
   !rec_eq_of_rel
 
@@ -120,7 +120,7 @@ section
 
   protected definition rec {P : seq_colim → Type}
     (Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a))
-    (Pglue : Π(n : ℕ) (a : A n), glue a ▹ Pincl (f a) = Pincl a) (aa : seq_colim) : P aa :=
+    (Pglue : Π(n : ℕ) (a : A n), glue a ▸ Pincl (f a) = Pincl a) (aa : seq_colim) : P aa :=
   begin
     fapply (type_quotient.rec_on aa),
     { intro a, cases a, apply Pincl},
@@ -129,12 +129,12 @@ section
 
   protected definition rec_on [reducible] {P : seq_colim → Type} (aa : seq_colim)
     (Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a))
-    (Pglue : Π⦃n : ℕ⦄ (a : A n), glue a ▹ Pincl (f a) = Pincl a)
+    (Pglue : Π⦃n : ℕ⦄ (a : A n), glue a ▸ Pincl (f a) = Pincl a)
       : P aa :=
   rec Pincl Pglue aa
 
   theorem rec_glue {P : seq_colim → Type} (Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a))
-    (Pglue : Π⦃n : ℕ⦄ (a : A n), glue a ▹ Pincl (f a) = Pincl a) {n : ℕ} (a : A n)
+    (Pglue : Π⦃n : ℕ⦄ (a : A n), glue a ▸ Pincl (f a) = Pincl a) {n : ℕ} (a : A n)
       : apd (rec Pincl Pglue) (glue a) = Pglue a :=
   !rec_eq_of_rel
 
diff --git a/hott/hit/cylinder.hlean b/hott/hit/cylinder.hlean
index ef8c7b88f..d18cb65d1 100644
--- a/hott/hit/cylinder.hlean
+++ b/hott/hit/cylinder.hlean
@@ -37,7 +37,7 @@ parameters {A B : Type.{u}} (f : A → B)
 
   protected definition rec {P : cylinder → Type}
     (Pbase : Π(b : B), P (base b)) (Ptop : Π(a : A), P (top a))
-    (Pseg : Π(a : A), seg a ▹ Pbase (f a) = Ptop a) (x : cylinder) : P x :=
+    (Pseg : Π(a : A), seg a ▸ Pbase (f a) = Ptop a) (x : cylinder) : P x :=
   begin
     fapply (type_quotient.rec_on x),
     { intro a, cases a,
@@ -48,12 +48,12 @@ parameters {A B : Type.{u}} (f : A → B)
 
   protected definition rec_on [reducible] {P : cylinder → Type} (x : cylinder)
     (Pbase : Π(b : B), P (base b)) (Ptop  : Π(a : A), P (top a))
-    (Pseg  : Π(a : A), seg a ▹ Pbase (f a) = Ptop a) : P x :=
+    (Pseg  : Π(a : A), seg a ▸ Pbase (f a) = Ptop a) : P x :=
   rec Pbase Ptop Pseg x
 
   theorem rec_seg {P : cylinder → Type}
     (Pbase : Π(b : B), P (base b)) (Ptop : Π(a : A), P (top a))
-    (Pseg : Π(a : A), seg a ▹ Pbase (f a) = Ptop a)
+    (Pseg : Π(a : A), seg a ▸ Pbase (f a) = Ptop a)
       (a : A) : apd (rec Pbase Ptop Pseg) (seg a) = Pseg a :=
   !rec_eq_of_rel
 
diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean
index 0dfdc2d68..0e7681121 100644
--- a/hott/hit/pushout.hlean
+++ b/hott/hit/pushout.hlean
@@ -35,7 +35,7 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR)
   eq_of_rel pushout_rel (Rmk f g x)
 
   protected definition rec {P : pushout → Type} (Pinl : Π(x : BL), P (inl x))
-    (Pinr : Π(x : TR), P (inr x)) (Pglue : Π(x : TL), glue x ▹ Pinl (f x) = Pinr (g x))
+    (Pinr : Π(x : TR), P (inr x)) (Pglue : Π(x : TL), glue x ▸ Pinl (f x) = Pinr (g x))
       (y : pushout) : P y :=
   begin
     fapply (type_quotient.rec_on y),
@@ -47,11 +47,11 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR)
 
   protected definition rec_on [reducible] {P : pushout → Type} (y : pushout)
     (Pinl : Π(x : BL), P (inl x)) (Pinr : Π(x : TR), P (inr x))
-    (Pglue : Π(x : TL), glue x ▹ Pinl (f x) = Pinr (g x)) : P y :=
+    (Pglue : Π(x : TL), glue x ▸ Pinl (f x) = Pinr (g x)) : P y :=
   rec Pinl Pinr Pglue y
 
   theorem rec_glue {P : pushout → Type} (Pinl : Π(x : BL), P (inl x))
-    (Pinr : Π(x : TR), P (inr x)) (Pglue : Π(x : TL), glue x ▹ Pinl (f x) = Pinr (g x))
+    (Pinr : Π(x : TR), P (inr x)) (Pglue : Π(x : TL), glue x ▸ Pinl (f x) = Pinr (g x))
       (x : TL) : apd (rec Pinl Pinr Pglue) (glue x) = Pglue x :=
   !rec_eq_of_rel
 
diff --git a/hott/hit/quotient.hlean b/hott/hit/quotient.hlean
index bfbfcd97d..281c64421 100644
--- a/hott/hit/quotient.hlean
+++ b/hott/hit/quotient.hlean
@@ -28,7 +28,7 @@ parameters {A : Type} (R : A → A → hprop)
   begin unfold quotient, exact _ end
 
   protected definition rec {P : quotient → Type} [Pt : Πaa, is_hset (P aa)]
-    (Pc : Π(a : A), P (class_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▹ Pc a = Pc a')
+    (Pc : Π(a : A), P (class_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▸ Pc a = Pc a')
     (x : quotient) : P x :=
   begin
     apply (@trunc.rec_on _ _ P x),
@@ -41,11 +41,11 @@ parameters {A : Type} (R : A → A → hprop)
 
   protected definition rec_on [reducible] {P : quotient → Type} (x : quotient)
     [Pt : Πaa, is_hset (P aa)] (Pc : Π(a : A), P (class_of a))
-    (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▹ Pc a = Pc a') : P x :=
+    (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▸ Pc a = Pc a') : P x :=
   rec Pc Pp x
 
   theorem rec_eq_of_rel {P : quotient → Type} [Pt : Πaa, is_hset (P aa)]
-    (Pc : Π(a : A), P (class_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▹ Pc a = Pc a')
+    (Pc : Π(a : A), P (class_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▸ Pc a = Pc a')
     {a a' : A} (H : R a a') : apd (rec Pc Pp) (eq_of_rel H) = Pp H :=
   !is_hset.elim
 
diff --git a/hott/hit/suspension.hlean b/hott/hit/suspension.hlean
index cb60900ae..0dcc91ba2 100644
--- a/hott/hit/suspension.hlean
+++ b/hott/hit/suspension.hlean
@@ -27,7 +27,7 @@ namespace suspension
   glue _ _ a
 
   protected definition rec {P : suspension A → Type} (PN : P !north) (PS : P !south)
-    (Pm : Π(a : A), merid a ▹ PN = PS) (x : suspension A) : P x :=
+    (Pm : Π(a : A), merid a ▸ PN = PS) (x : suspension A) : P x :=
   begin
     fapply (pushout.rec_on _ _ x),
     { intro u, cases u, exact PN},
@@ -36,11 +36,11 @@ namespace suspension
   end
 
   protected definition rec_on [reducible] {P : suspension A → Type} (y : suspension A)
-    (PN : P !north) (PS : P !south) (Pm : Π(a : A), merid a ▹ PN = PS) : P y :=
+    (PN : P !north) (PS : P !south) (Pm : Π(a : A), merid a ▸ PN = PS) : P y :=
   rec PN PS Pm y
 
   theorem rec_merid {P : suspension A → Type} (PN : P !north) (PS : P !south)
-    (Pm : Π(a : A), merid a ▹ PN = PS) (a : A)
+    (Pm : Π(a : A), merid a ▸ PN = PS) (a : A)
       : apd (rec PN PS Pm) (merid a) = Pm a :=
   !rec_glue
 
diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean
index 9072275fa..4b648a40b 100644
--- a/hott/init/equiv.hlean
+++ b/hott/init/equiv.hlean
@@ -268,8 +268,8 @@ namespace equiv
 
   -- calc enviroment
   -- Note: Calculating with substitutions needs univalence
-  definition equiv_of_equiv_of_eq {A B C : Type} (p : A = B) (q : B ≃ C) : A ≃ C := p⁻¹ ▹ q
-  definition equiv_of_eq_of_equiv {A B C : Type} (p : A ≃ B) (q : B = C) : A ≃ C := q   ▹ p
+  definition equiv_of_equiv_of_eq {A B C : Type} (p : A = B) (q : B ≃ C) : A ≃ C := p⁻¹ ▸ q
+  definition equiv_of_eq_of_equiv {A B C : Type} (p : A ≃ B) (q : B = C) : A ≃ C := q   ▸ p
 
   attribute equiv.trans [trans]
   attribute equiv.refl [refl]
diff --git a/hott/init/funext.hlean b/hott/init/funext.hlean
index 39da9f104..63b81869f 100644
--- a/hott/init/funext.hlean
+++ b/hott/init/funext.hlean
@@ -86,7 +86,7 @@ section
   local attribute weak_funext [reducible]
   local attribute homotopy_ind [reducible]
   definition homotopy_ind_comp : homotopy_ind f (homotopy.refl f) = d :=
-    (@hprop_eq_of_is_contr _ _ _ _ !eq_of_is_contr idp)⁻¹ ▹ idp
+    (@hprop_eq_of_is_contr _ _ _ _ !eq_of_is_contr idp)⁻¹ ▸ idp
 end
 
 /- Now the proof is fairly easy; we can just use the same induction principle on both sides. -/
@@ -135,9 +135,9 @@ section
               B p (λ x', idp))
             ) eqinv x,
         have eqfin' : (to_fun w') ∘ ((to_fun eq')⁻¹ ∘ x) = x,
-          from eqretr ▹ eqfin,
+          from eqretr ▸ eqfin,
         have eqfin'' : (to_fun w') ∘ ((to_fun w')⁻¹ ∘ x) = x,
-          from invs_eq ▹ eqfin',
+          from invs_eq ▸ eqfin',
         eqfin''
       )
       (λ (x : C → A),
@@ -148,9 +148,9 @@ section
         have eqfin : (to_fun eq')⁻¹ ∘ ((to_fun eq') ∘ x) = x,
           from (λ p, eq.rec_on p idp) eqinv,
         have eqfin' : (to_fun eq')⁻¹ ∘ ((to_fun w') ∘ x) = x,
-          from eqretr ▹ eqfin,
+          from eqretr ▸ eqfin,
         have eqfin'' : (to_fun w')⁻¹ ∘ ((to_fun w') ∘ x) = x,
-          from invs_eq ▹ eqfin',
+          from invs_eq ▸ eqfin',
         eqfin''
       )
 
@@ -257,4 +257,4 @@ definition naive_funext_of_ua : naive_funext :=
 
 protected definition homotopy.rec_on {Q : (f ∼ g) → Type} (p : f ∼ g)
   (H : Π(q : f = g), Q (apd10 q)) : Q p :=
-right_inv apd10 p ▹ H (eq_of_homotopy p)
+right_inv apd10 p ▸ H (eq_of_homotopy p)
diff --git a/hott/init/hit.hlean b/hott/init/hit.hlean
index 4fe0daf02..aa496467e 100644
--- a/hott/init/hit.hlean
+++ b/hott/init/hit.hlean
@@ -56,12 +56,12 @@ namespace type_quotient
     : class_of R a = class_of R a'
 
   protected constant rec {A : Type} {R : A → A → Type} {P : type_quotient R → Type}
-    (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel R H ▹ Pc a = Pc a')
+    (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel R H ▸ Pc a = Pc a')
     (x : type_quotient R) : P x
 
   protected definition rec_on [reducible] {A : Type} {R : A → A → Type} {P : type_quotient R → Type}
     (x : type_quotient R) (Pc : Π(a : A), P (class_of R a))
-    (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel R H ▹ Pc a = Pc a') : P x :=
+    (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel R H ▸ Pc a = Pc a') : P x :=
   rec Pc Pp x
 
 end type_quotient
@@ -76,11 +76,11 @@ end trunc
 
 namespace type_quotient
   definition rec_class_of {A : Type} {R : A → A → Type} {P : type_quotient R → Type}
-    (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel R H ▹ Pc a = Pc a')
+    (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel R H ▸ Pc a = Pc a')
     (a : A) : type_quotient.rec Pc Pp (class_of R a) = Pc a :=
   idp
 
   constant rec_eq_of_rel {A : Type} {R : A → A → Type} {P : type_quotient R → Type}
-    (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel R H ▹ Pc a = Pc a')
+    (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel R H ▸ Pc a = Pc a')
     {a a' : A} (H : R a a') : apd (type_quotient.rec Pc Pp) (eq_of_rel R H) = Pp H
 end type_quotient
diff --git a/hott/init/path.hlean b/hott/init/path.hlean
index 126614750..bcd2ab798 100644
--- a/hott/init/path.hlean
+++ b/hott/init/path.hlean
@@ -182,13 +182,13 @@ namespace eq
   eq.rec_on p u
 
   -- This idiom makes the operation right associative.
-  notation p `▹`:65 x:64 := transport _ p x
+  notation p `▸` x := transport _ p x
 
   definition cast [reducible] {A B : Type} (p : A = B) (a : A) : B :=
-  p ▹ a
+  p ▸ a
 
   definition tr_inv [reducible] (P : A → Type) {x y : A} (p : x = y) (u : P y) : P x :=
-  p⁻¹ ▹ u
+  p⁻¹ ▸ u
 
   definition ap ⦃A B : Type⦄ (f : A → B) {x y:A} (p : x = y) : f x = f y :=
   eq.rec_on p idp
@@ -223,7 +223,7 @@ namespace eq
   definition ap11 {f g : A → B} (H : f = g) {x y : A} (p : x = y) : f x = g y :=
   eq.rec_on H (eq.rec_on p idp)
 
-  definition apd (f : Πa:A, P a) {x y : A} (p : x = y) : p ▹ f x = f y :=
+  definition apd (f : Πa:A, P a) {x y : A} (p : x = y) : p ▸ f x = f y :=
   eq.rec_on p idp
 
   /- calc enviroment -/
@@ -235,19 +235,19 @@ namespace eq
   /- More theorems for moving things around in equations -/
 
   definition tr_eq_of_eq_inv_tr {P : A → Type} {x y : A} {p : x = y} {u : P x} {v : P y} :
-    u = p⁻¹ ▹ v → p ▹ u = v :=
+    u = p⁻¹ ▸ v → p ▸ u = v :=
   eq.rec_on p (take v, id) v
 
   definition inv_tr_eq_of_eq_tr {P : A → Type} {x y : A} {p : y = x} {u : P x} {v : P y} :
-    u = p ▹ v → p⁻¹ ▹ u = v :=
+    u = p ▸ v → p⁻¹ ▸ u = v :=
   eq.rec_on p (take u, id) u
 
   definition eq_inv_tr_of_tr_eq {P : A → Type} {x y : A} {p : x = y} {u : P x} {v : P y} :
-    p ▹ u = v → u = p⁻¹ ▹ v :=
+    p ▸ u = v → u = p⁻¹ ▸ v :=
   eq.rec_on p (take v, id) v
 
   definition eq_tr_of_inv_tr_eq {P : A → Type} {x y : A} {p : y = x} {u : P x} {v : P y} :
-    p⁻¹ ▹ u = v → u = p ▹ v :=
+    p⁻¹ ▸ u = v → u = p ▸ v :=
   eq.rec_on p (take u, id) u
 
   /- Functoriality of functions -/
@@ -332,7 +332,7 @@ namespace eq
         ... = p x : !idp_con
         ... = (p x) ⬝ (ap g idp ⬝ idp) : idp))
   -- This also works:
-  -- eq.rec_on s (eq.rec_on q (!idp_con ▹ idp))
+  -- eq.rec_on s (eq.rec_on q (!idp_con ▸ idp))
 
   definition con_ap_con_con_eq_con_con_con {f : A → A} (p : f ∼ id) {x y : A} (q : x = y)
       {w z : A} (r : w = f x) (s : y = z) :
@@ -352,7 +352,7 @@ namespace eq
   definition ap_con_con_eq_con_con {f : A → A} (p : f ∼ id) {x y : A} (q : x = y)
       {z : A} (s : y = z) :
     ap f q ⬝ (p y ⬝ s) = p x ⬝ (q ⬝ s) :=
-  eq.rec_on s (eq.rec_on q (!idp_con ▹ idp))
+  eq.rec_on s (eq.rec_on q (!idp_con ▸ idp))
 
   definition con_con_ap_eq_con_con {g : A → A} (p : id ∼ g) {x y : A} (q : x = y)
       {w : A} (r : w = x) :
@@ -365,7 +365,7 @@ namespace eq
   begin
     apply (eq.rec_on s),
     apply (eq.rec_on q),
-    apply (idp_con (p x) ▹ idp)
+    apply (idp_con (p x) ▸ idp)
   end
 
   /- Action of [apd10] and [ap10] on paths -/
@@ -398,26 +398,26 @@ namespace eq
 
   /- Transport and the groupoid structure of paths -/
 
-  definition idp_tr {P : A → Type} {x : A} (u : P x) : idp ▹ u = u := idp
+  definition idp_tr {P : A → Type} {x : A} (u : P x) : idp ▸ u = u := idp
 
   definition con_tr {P : A → Type} {x y z : A} (p : x = y) (q : y = z) (u : P x) :
-    p ⬝ q ▹ u = q ▹ p ▹ u :=
+    p ⬝ q ▸ u = q ▸ p ▸ u :=
   eq.rec_on q (eq.rec_on p idp)
 
   definition tr_inv_tr {P : A → Type} {x y : A} (p : x = y) (z : P y) :
-    p ▹ p⁻¹ ▹ z = z :=
+    p ▸ p⁻¹ ▸ z = z :=
   (con_tr p⁻¹ p z)⁻¹ ⬝ ap (λr, transport P r z) (con.left_inv p)
 
   definition inv_tr_tr {P : A → Type} {x y : A} (p : x = y) (z : P x) :
-    p⁻¹ ▹ p ▹ z = z :=
+    p⁻¹ ▸ p ▸ z = z :=
   (con_tr p p⁻¹ z)⁻¹ ⬝ ap (λr, transport P r z) (con.right_inv p)
 
   definition con_tr_lemma {P : A → Type}
       {x y z w : A} (p : x = y) (q : y = z) (r : z = w) (u : P x) :
-    ap (λe, e ▹ u) (con.assoc' p q r) ⬝ (con_tr (p ⬝ q) r u) ⬝
+    ap (λe, e ▸ u) (con.assoc' p q r) ⬝ (con_tr (p ⬝ q) r u) ⬝
         ap (transport P r) (con_tr p q u)
-      = (con_tr p (q ⬝ r) u) ⬝ (con_tr q r (p ▹ u))
-      :> ((p ⬝ (q ⬝ r)) ▹ u = r ▹ q ▹ p ▹ u) :=
+      = (con_tr p (q ⬝ r) u) ⬝ (con_tr q r (p ▸ u))
+      :> ((p ⬝ (q ⬝ r)) ▸ u = r ▸ q ▸ p ▸ u) :=
   eq.rec_on r (eq.rec_on q (eq.rec_on p idp))
 
   --  Here is another coherence lemma for transport.
@@ -438,18 +438,18 @@ namespace eq
 
   -- Dependent transport in a doubly dependent type.
   definition transportD {P : A → Type} (Q : Π a : A, P a → Type)
-      {a a' : A} (p : a = a') (b : P a) (z : Q a b) : Q a' (p ▹ b) :=
+      {a a' : A} (p : a = a') (b : P a) (z : Q a b) : Q a' (p ▸ b) :=
   eq.rec_on p z
 
   -- In Coq the variables P, Q and b are explicit, but in Lean we can probably have them implicit using the following notation
-  notation p `▹D`:65 x:64 := transportD _ p _ x
+  notation p `▸D`:65 x:64 := transportD _ p _ x
 
   -- Transporting along higher-dimensional paths
   definition transport2 (P : A → Type) {x y : A} {p q : x = y} (r : p = q) (z : P x) :
-    p ▹ z = q ▹ z :=
-  ap (λp', p' ▹ z) r
+    p ▸ z = q ▸ z :=
+  ap (λp', p' ▸ z) r
 
-  notation p `▹2`:65 x:64 := transport2 _ p _ x
+  notation p `▸2`:65 x:64 := transport2 _ p _ x
 
   -- An alternative definition.
   definition tr2_eq_ap10 (Q : A → Type) {x y : A} {p q : x = y} (r : p = q)
@@ -467,10 +467,10 @@ namespace eq
   eq.rec_on r idp
 
   definition transportD2 (B C : A → Type) (D : Π(a:A), B a → C a → Type)
-    {x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C x1) (w : D x1 y z) : D x2 (p ▹ y) (p ▹ z) :=
+    {x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C x1) (w : D x1 y z) : D x2 (p ▸ y) (p ▸ z) :=
   eq.rec_on p w
 
-  notation p `▹D2`:65 x:64 := transportD2 _ _ _ p _ _ x
+  notation p `▸D2`:65 x:64 := transportD2 _ _ _ p _ _ x
 
   definition ap_tr_con_tr2 (P : A → Type) {x y : A} {p q : x = y} {z w : P x} (r : p = q)
       (s : z = w) :
@@ -479,7 +479,7 @@ namespace eq
 
 
   definition fn_tr_eq_tr_fn {P Q : A → Type} {x y : A} (p : x = y) (f : Πx, P x → Q x) (z : P x) :
-    f y (p ▹ z) = (p ▹ (f x z)) :=
+    f y (p ▸ z) = (p ▸ (f x z)) :=
   eq.rec_on p idp
 
   /- Transporting in particular fibrations -/
@@ -520,7 +520,7 @@ namespace eq
   eq.rec_on p idp
 
   -- A special case of [transport_compose] which seems to come up a lot.
-  definition tr_eq_cast_ap {P : A → Type} {x y} (p : x = y) (u : P x) : p ▹ u = cast (ap P p) u :=
+  definition tr_eq_cast_ap {P : A → Type} {x y} (p : x = y) (u : P x) : p ▸ u = cast (ap P p) u :=
   eq.rec_on p idp
 
   definition tr_eq_cast_ap_fn {P : A → Type} {x y} (p : x = y) : transport P p = cast (ap P p) :=
diff --git a/hott/init/ua.hlean b/hott/init/ua.hlean
index 7312a6759..4ade28d1c 100644
--- a/hott/init/ua.hlean
+++ b/hott/init/ua.hlean
@@ -61,6 +61,6 @@ namespace equiv
 
   definition rec_on_of_equiv_of_eq {A B : Type} {P : (A ≃ B) → Type}
     (p : A ≃ B) (H : Π(q : A = B), P (equiv_of_eq q)) : P p :=
-  right_inv equiv_of_eq p ▹ H (ua p)
+  right_inv equiv_of_eq p ▸ H (ua p)
 
 end equiv
diff --git a/hott/types/W.hlean b/hott/types/W.hlean
index 989be8f38..d7b7d3cd5 100644
--- a/hott/types/W.hlean
+++ b/hott/types/W.hlean
@@ -40,10 +40,10 @@ namespace Wtype
   protected definition eta (w : W a, B a) : ⟨w.1 , w.2⟩ = w :=
   cases_on w (λa f, idp)
 
-  definition sup_eq_sup (p : a = a') (q : p ▹ f = f') : ⟨a, f⟩ = ⟨a', f'⟩ :=
+  definition sup_eq_sup (p : a = a') (q : p ▸ f = f') : ⟨a, f⟩ = ⟨a', f'⟩ :=
   path.rec_on p (λf' q, path.rec_on q idp) f' q
 
-  protected definition Wtype_eq (p : w.1 = w'.1) (q : p ▹ w.2 = w'.2) : w = w' :=
+  protected definition Wtype_eq (p : w.1 = w'.1) (q : p ▸ w.2 = w'.2) : w = w' :=
   cases_on w
            (λw1 w2, cases_on w' (λ w1' w2', sup_eq_sup))
            p q
@@ -51,7 +51,7 @@ namespace Wtype
   protected definition Wtype_eq_pr1 (p : w = w') : w.1 = w'.1 :=
   path.rec_on p idp
 
-  protected definition Wtype_eq_pr2 (p : w = w') : Wtype_eq_pr1 p ▹ w.2 = w'.2 :=
+  protected definition Wtype_eq_pr2 (p : w = w') : Wtype_eq_pr1 p ▸ w.2 = w'.2 :=
   path.rec_on p idp
 
   namespace ops
@@ -60,7 +60,7 @@ namespace Wtype
   end ops
   open ops
 
-  definition sup_path_W (p : w.1 = w'.1) (q : p ▹ w.2 = w'.2)
+  definition sup_path_W (p : w.1 = w'.1) (q : p ▸ w.2 = w'.2)
       :  dpair (Wtype_eq p q)..1 (Wtype_eq p q)..2 = dpair p q :=
   begin
     revert p q,
@@ -70,11 +70,11 @@ namespace Wtype
     apply (path.rec_on q), apply idp
   end
 
-  definition pr1_path_W (p : w.1 = w'.1) (q : p ▹ w.2 = w'.2) : (Wtype_eq p q)..1 = p :=
+  definition pr1_path_W (p : w.1 = w'.1) (q : p ▸ w.2 = w'.2) : (Wtype_eq p q)..1 = p :=
   (!sup_path_W)..1
 
-  definition pr2_path_W (p : w.1 = w'.1) (q : p ▹ w.2 = w'.2)
-      : pr1_path_W p q ▹ (Wtype_eq p q)..2 = q :=
+  definition pr2_path_W (p : w.1 = w'.1) (q : p ▸ w.2 = w'.2)
+      : pr1_path_W p q ▸ (Wtype_eq p q)..2 = q :=
   (!sup_path_W)..2
 
   definition eta_path_W (p : w = w') : Wtype_eq (p..1) (p..2) = p :=
@@ -84,7 +84,7 @@ namespace Wtype
     apply idp
   end
 
-  definition transport_pr1_path_W {B' : A → Type} (p : w.1 = w'.1) (q : p ▹ w.2 = w'.2)
+  definition transport_pr1_path_W {B' : A → Type} (p : w.1 = w'.1) (q : p ▸ w.2 = w'.2)
       : transport (λx, B' x.1) (Wtype_eq p q) = transport B' p :=
   begin
     revert p q,
@@ -94,25 +94,25 @@ namespace Wtype
     apply (path.rec_on q), apply idp
   end
 
-  definition path_W_uncurried (pq : Σ(p : w.1 = w'.1), p ▹ w.2 = w'.2) : w = w' :=
+  definition path_W_uncurried (pq : Σ(p : w.1 = w'.1), p ▸ w.2 = w'.2) : w = w' :=
   destruct pq Wtype_eq
 
-  definition sup_path_W_uncurried (pq : Σ(p : w.1 = w'.1), p ▹ w.2 = w'.2)
+  definition sup_path_W_uncurried (pq : Σ(p : w.1 = w'.1), p ▸ w.2 = w'.2)
       :  dpair (path_W_uncurried pq)..1 (path_W_uncurried pq)..2 = pq :=
   destruct pq sup_path_W
 
-  definition pr1_path_W_uncurried (pq : Σ(p : w.1 = w'.1), p ▹ w.2 = w'.2)
+  definition pr1_path_W_uncurried (pq : Σ(p : w.1 = w'.1), p ▸ w.2 = w'.2)
       : (path_W_uncurried pq)..1 = pq.1 :=
   (!sup_path_W_uncurried)..1
 
-  definition pr2_path_W_uncurried (pq : Σ(p : w.1 = w'.1), p ▹ w.2 = w'.2)
-      : (pr1_path_W_uncurried pq) ▹ (path_W_uncurried pq)..2 = pq.2 :=
+  definition pr2_path_W_uncurried (pq : Σ(p : w.1 = w'.1), p ▸ w.2 = w'.2)
+      : (pr1_path_W_uncurried pq) ▸ (path_W_uncurried pq)..2 = pq.2 :=
   (!sup_path_W_uncurried)..2
 
   definition eta_path_W_uncurried (p : w = w') : path_W_uncurried (dpair p..1 p..2) = p :=
   !eta_path_W
 
-  definition transport_pr1_path_W_uncurried {B' : A → Type} (pq : Σ(p : w.1 = w'.1), p ▹ w.2 = w'.2)
+  definition transport_pr1_path_W_uncurried {B' : A → Type} (pq : Σ(p : w.1 = w'.1), p ▸ w.2 = w'.2)
       : transport (λx, B' x.1) (@path_W_uncurried A B w w' pq) = transport B' pq.1 :=
     destruct pq transport_pr1_path_W
 
@@ -123,7 +123,7 @@ namespace Wtype
              eta_path_W_uncurried
              sup_path_W_uncurried
 
-  definition equiv_path_W (w w' : W a, B a) : (Σ(p : w.1 = w'.1),  p ▹ w.2 = w'.2) ≃ (w = w') :=
+  definition equiv_path_W (w w' : W a, B a) : (Σ(p : w.1 = w'.1),  p ▸ w.2 = w'.2) ≃ (w = w') :=
   equiv.mk path_W_uncurried !isequiv_path_W
 
   definition double_induction_on {P : (W a, B a) → (W a, B a) → Type} (w w' : W a, B a)
diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean
index b42e3f395..64261edd2 100644
--- a/hott/types/pi.hlean
+++ b/hott/types/pi.hlean
@@ -52,7 +52,7 @@ namespace pi
 
   definition pi_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],
@@ -78,22 +78,22 @@ namespace pi
      (Π(b : B a), transportD B C p b (f b) = g (transport B p b)) ≃
      (transport (λa, Π(b : B a), C a b) p f = g) -/
   definition heq_piD (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) :=
+    (g : Π(b' : B a'), C a' b') : (Π(b : B a), p ▸D (f b) = g (p ▸ b)) ≃ (p ▸ f = g) :=
   eq.rec_on p (λg, !homotopy_equiv_eq) g
 
   definition heq_pi {C : A → Type} (p : a = a') (f : Π(b : B a), C a)
-    (g : Π(b' : B a'), C a') : (Π(b : B a), p ▹ (f b) = g (p ▹ b)) ≃ (p ▹ f = g) :=
+    (g : Π(b' : B a'), C a') : (Π(b : B a), p ▸ (f b) = g (p ▸ b)) ≃ (p ▸ f = g) :=
   eq.rec_on p (λg, !homotopy_equiv_eq) g
 
 
   section
   open sigma sigma.ops
   /- more implicit arguments:
-  (Π(b : B a), transport C (sigma_eq p idp) (f b) = g (p ▹ b)) ≃
+  (Π(b : B a), transport C (sigma_eq 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 (transport B p b)) -/
   definition heq_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_eq p idp) ▹ (f b) = g (p ▹ b)) ≃ (Π(b : B a), p ▹D (f b) = g (p ▹ b)) :=
+    (Π(b : B a), (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
 
@@ -129,13 +129,13 @@ namespace pi
       apply (tr_inv _ (adj f0 a')),
       apply (transport (λx, f1 a' x = h a') (transport_compose B f0 (left_inv f0 a') _)),
       apply (tr_inv (λx, x = h a') (fn_tr_eq_tr_fn _ f1 _)), unfold function.compose,
-      apply (tr_inv (λx, left_inv f0 a' ▹ x = h a') (right_inv (f1 _) _)), unfold function.id,
+      apply (tr_inv (λx, left_inv f0 a' ▸ x = h a') (right_inv (f1 _) _)), unfold function.id,
       apply apd
     end,
     begin
       intro h,
       apply eq_of_homotopy, intro a,
-      apply (tr_inv (λx, right_inv f0 a ▹ x = h a) (left_inv (f1 _) _)), unfold function.id,
+      apply (tr_inv (λx, right_inv f0 a ▸ x = h a) (left_inv (f1 _) _)), unfold function.id,
       apply apd
     end
   end
diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean
index 8bba7fa6a..23a290040 100644
--- a/hott/types/sigma.hlean
+++ b/hott/types/sigma.hlean
@@ -28,10 +28,10 @@ namespace sigma
   definition eta3 : Π (u : Σa b c, D a b c), ⟨u.1, u.2.1, u.2.2.1, u.2.2.2⟩ = u
   | eta3 ⟨u₁, u₂, u₃, u₄⟩ := idp
 
-  definition dpair_eq_dpair (p : a = a') (q : p ▹ b = b') : ⟨a, b⟩ = ⟨a', b'⟩ :=
+  definition dpair_eq_dpair (p : a = a') (q : p ▸ b = b') : ⟨a, b⟩ = ⟨a', b'⟩ :=
   by cases p; cases q; reflexivity
 
-  definition sigma_eq (p : u.1 = v.1) (q : p ▹ u.2 = v.2) : u = v :=
+  definition sigma_eq (p : u.1 = v.1) (q : p ▸ u.2 = v.2) : u = v :=
   by cases u; cases v; apply (dpair_eq_dpair p q)
 
   /- Projections of paths from a total space -/
@@ -41,51 +41,51 @@ namespace sigma
 
   postfix `..1`:(max+1) := eq_pr1
 
-  definition eq_pr2 (p : u = v) : p..1 ▹ u.2 = v.2 :=
+  definition eq_pr2 (p : u = v) : p..1 ▸ u.2 = v.2 :=
   by cases p; reflexivity
 
   postfix `..2`:(max+1) := eq_pr2
 
-  private definition dpair_sigma_eq (p : u.1 = v.1) (q : p ▹ u.2 = v.2)
+  private definition dpair_sigma_eq (p : u.1 = v.1) (q : p ▸ u.2 = v.2)
       : ⟨(sigma_eq p q)..1, (sigma_eq p q)..2⟩ = ⟨p, q⟩ :=
-  by cases u; cases v; cases p; cases q; reflexivity
+  by cases u; cases v; cases p; cases q; apply idp
 
-  definition sigma_eq_pr1 (p : u.1 = v.1) (q : p ▹ u.2 = v.2) : (sigma_eq p q)..1 = p :=
+  definition sigma_eq_pr1 (p : u.1 = v.1) (q : p ▸ u.2 = v.2) : (sigma_eq p q)..1 = p :=
   (dpair_sigma_eq p q)..1
 
-  definition sigma_eq_pr2 (p : u.1 = v.1) (q : p ▹ u.2 = v.2)
-      : sigma_eq_pr1 p q ▹ (sigma_eq p q)..2 = q :=
+  definition sigma_eq_pr2 (p : u.1 = v.1) (q : p ▸ u.2 = v.2)
+      : sigma_eq_pr1 p q ▸ (sigma_eq p q)..2 = q :=
   (dpair_sigma_eq p q)..2
 
   definition sigma_eq_eta (p : u = v) : sigma_eq (p..1) (p..2) = p :=
   by cases p; cases u; reflexivity
 
-  definition tr_pr1_sigma_eq {B' : A → Type} (p : u.1 = v.1) (q : p ▹ u.2 = v.2)
+  definition tr_pr1_sigma_eq {B' : A → Type} (p : u.1 = v.1) (q : p ▸ u.2 = v.2)
       : transport (λx, B' x.1) (sigma_eq p q) = transport B' p :=
   by cases u; cases v; cases p; cases q; reflexivity
 
   /- the uncurried version of sigma_eq. We will prove that this is an equivalence -/
 
-  definition sigma_eq_uncurried : Π (pq : Σ(p : u.1 = v.1), p ▹ u.2 = v.2), u = v
+  definition sigma_eq_uncurried : Π (pq : Σ(p : u.1 = v.1), p ▸ u.2 = v.2), u = v
   | sigma_eq_uncurried ⟨pq₁, pq₂⟩ := sigma_eq pq₁ pq₂
 
-  definition dpair_sigma_eq_uncurried : Π (pq : Σ(p : u.1 = v.1), p ▹ u.2 = v.2),
+  definition dpair_sigma_eq_uncurried : Π (pq : Σ(p : u.1 = v.1), p ▸ u.2 = v.2),
         ⟨(sigma_eq_uncurried pq)..1, (sigma_eq_uncurried pq)..2⟩ = pq
   | dpair_sigma_eq_uncurried ⟨pq₁, pq₂⟩ := dpair_sigma_eq pq₁ pq₂
 
-  definition sigma_eq_pr1_uncurried (pq : Σ(p : u.1 = v.1), p ▹ u.2 = v.2)
+  definition sigma_eq_pr1_uncurried (pq : Σ(p : u.1 = v.1), p ▸ u.2 = v.2)
       : (sigma_eq_uncurried pq)..1 = pq.1 :=
   (dpair_sigma_eq_uncurried pq)..1
 
-  definition sigma_eq_pr2_uncurried (pq : Σ(p : u.1 = v.1), p ▹ u.2 = v.2)
-      : (sigma_eq_pr1_uncurried pq) ▹ (sigma_eq_uncurried pq)..2 = pq.2 :=
+  definition sigma_eq_pr2_uncurried (pq : Σ(p : u.1 = v.1), p ▸ u.2 = v.2)
+      : (sigma_eq_pr1_uncurried pq) ▸ (sigma_eq_uncurried pq)..2 = pq.2 :=
   (dpair_sigma_eq_uncurried pq)..2
 
   definition sigma_eq_eta_uncurried (p : u = v) : sigma_eq_uncurried ⟨p..1, p..2⟩ = p :=
   sigma_eq_eta p
 
   definition tr_sigma_eq_pr1_uncurried {B' : A → Type}
-    (pq : Σ(p : u.1 = v.1), p ▹ u.2 = v.2)
+    (pq : Σ(p : u.1 = v.1), p ▸ u.2 = v.2)
       : transport (λx, B' x.1) (@sigma_eq_uncurried A B u v pq) = transport B' pq.1 :=
   destruct pq tr_pr1_sigma_eq
 
@@ -96,23 +96,23 @@ namespace sigma
              sigma_eq_eta_uncurried
              dpair_sigma_eq_uncurried
 
-  definition equiv_sigma_eq (u v : Σa, B a) : (Σ(p : u.1 = v.1),  p ▹ u.2 = v.2) ≃ (u = v) :=
+  definition equiv_sigma_eq (u v : Σa, B a) : (Σ(p : u.1 = v.1),  p ▸ u.2 = v.2) ≃ (u = v) :=
   equiv.mk sigma_eq_uncurried !is_equiv_sigma_eq
 
-  definition dpair_eq_dpair_con (p1 : a  = a' ) (q1 : p1 ▹ b  = b' )
-                                  (p2 : a' = a'') (q2 : p2 ▹ b' = b'') :
+  definition dpair_eq_dpair_con (p1 : a  = a' ) (q1 : p1 ▸ b  = b' )
+                                  (p2 : a' = a'') (q2 : p2 ▸ b' = b'') :
       dpair_eq_dpair (p1 ⬝ p2) (con_tr p1 p2 b ⬝ ap (transport B p2) q1 ⬝ q2)
     = dpair_eq_dpair p1 q1 ⬝ dpair_eq_dpair  p2 q2 :=
   by cases p1; cases p2; cases q1; cases q2; reflexivity
 
-  definition sigma_eq_con (p1 : u.1 = v.1) (q1 : p1 ▹ u.2 = v.2)
-                              (p2 : v.1 = w.1) (q2 : p2 ▹ v.2 = w.2) :
+  definition sigma_eq_con (p1 : u.1 = v.1) (q1 : p1 ▸ u.2 = v.2)
+                              (p2 : v.1 = w.1) (q2 : p2 ▸ v.2 = w.2) :
       sigma_eq (p1 ⬝ p2) (con_tr p1 p2 u.2 ⬝ ap (transport B p2) q1 ⬝ q2)
     = sigma_eq p1 q1 ⬝ sigma_eq p2 q2 :=
   by cases u; cases v; cases w; apply dpair_eq_dpair_con
 
   local attribute dpair_eq_dpair [reducible]
-  definition dpair_eq_dpair_con_idp (p : a = a') (q : p ▹ b = b') :
+  definition dpair_eq_dpair_con_idp (p : a = a') (q : p ▸ b = b') :
       dpair_eq_dpair p q = dpair_eq_dpair p idp ⬝ dpair_eq_dpair idp q :=
   by cases p; cases q; reflexivity
 
@@ -130,15 +130,15 @@ namespace sigma
   /- Dependent transport is the same as transport along a sigma_eq. -/
 
   definition transportD_eq_transport (p : a = a') (c : C a b) :
-      p ▹D c = transport (λu, C (u.1) (u.2)) (dpair_eq_dpair p idp) c :=
+      p ▸D c = transport (λu, C (u.1) (u.2)) (dpair_eq_dpair p idp) c :=
   by cases p; reflexivity
 
-  definition sigma_eq_eq_sigma_eq {p1 q1 : a = a'} {p2 : p1 ▹ b = b'} {q2 : q1 ▹ b = b'}
-      (r : p1 = q1) (s : r ▹ p2 = q2) : sigma_eq p1 p2 = sigma_eq q1 q2 :=
+  definition sigma_eq_eq_sigma_eq {p1 q1 : a = a'} {p2 : p1 ▸ b = b'} {q2 : q1 ▸ b = b'}
+      (r : p1 = q1) (s : r ▸ p2 = q2) : sigma_eq p1 p2 = sigma_eq q1 q2 :=
   by cases r; cases s; reflexivity
 
   /- A path between paths in a total space is commonly shown component wise. -/
-  definition sigma_eq2 {p q : u = v} (r : p..1 = q..1) (s : r ▹ p..2 = q..2)
+  definition sigma_eq2 {p q : u = v} (r : p..1 = q..1) (s : r ▸ p..2 = q..2)
     : p = q :=
   begin
     revert q r s,
@@ -161,18 +161,18 @@ namespace sigma
   In particular, this indicates why `transport` alone cannot be fully defined by induction on the structure of types, although Id-elim/transportD can be (cf. Observational Type Theory).  A more thorough set of lemmas, along the lines of the present ones but dealing with Id-elim rather than just transport, might be nice to have eventually? -/
 
   definition transport_eq (p : a = a') (bc : Σ(b : B a), C a b)
-      : p ▹ bc = ⟨p ▹ bc.1, p ▹D bc.2⟩ :=
+      : p ▸ bc = ⟨p ▸ bc.1, p ▸D bc.2⟩ :=
   by cases p; cases bc; reflexivity
 
   /- The special case when the second variable doesn't depend on the first is simpler. -/
   definition tr_eq_nondep {B : Type} {C : A → B → Type} (p : a = a') (bc : Σ(b : B), C a b)
-      : p ▹ bc = ⟨bc.1, p ▹ bc.2⟩ :=
+      : p ▸ bc = ⟨bc.1, p ▸ bc.2⟩ :=
   by cases p; cases bc; reflexivity
 
   /- Or if the second variable contains a first component that doesn't depend on the first. -/
 
   definition tr_eq2_nondep {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⟩ :=
+      (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
     cases p, cases bcd with b cd, cases cd, reflexivity
   end
@@ -198,7 +198,7 @@ namespace sigma
   -- end
     -- "rewrite right_inv (g (f⁻¹ a'))"
     apply concat, apply (ap (λx, (transport B' (right_inv f a') x))), apply (right_inv (g (f⁻¹ a'))),
-    show right_inv f a' ▹ ((right_inv f a')⁻¹ ▹ b') = b',
+    show right_inv f a' ▸ ((right_inv f a')⁻¹ ▸ b') = b',
     from tr_inv_tr (right_inv f a') b'
   end
   begin
@@ -233,13 +233,13 @@ namespace sigma
   definition sigma_equiv_sigma_id {B' : A → Type} (Hg : Π a, B a ≃ B' a) : (Σa, B a) ≃ Σa, B' a :=
   sigma_equiv_sigma equiv.refl Hg
 
-  definition ap_sigma_functor_eq_dpair (p : a = a') (q : p ▹ b = b')
+  definition ap_sigma_functor_eq_dpair (p : a = a') (q : p ▸ b = b')
     : ap (sigma.sigma_functor f g) (sigma_eq p q)
     = sigma_eq (ap f p)
                  ((transport_compose _ f p (g a b))⁻¹ ⬝ (fn_tr_eq_tr_fn p g b)⁻¹ ⬝ ap (g a') q) :=
   by cases p; cases q; reflexivity
 
-  definition ap_sigma_functor_eq (p : u.1 = v.1) (q : p ▹ u.2 = v.2)
+  definition ap_sigma_functor_eq (p : u.1 = v.1) (q : p ▸ u.2 = v.2)
     : ap (sigma.sigma_functor f g) (sigma_eq p q) =
       sigma_eq (ap f p)
        ((transport_compose B' f p (g u.1 u.2))⁻¹ ⬝ (fn_tr_eq_tr_fn p g u.2)⁻¹ ⬝ ap (g v.1) q) :=
@@ -262,9 +262,9 @@ namespace sigma
   definition sigma_equiv_of_is_contr_pr1 (B : A → Type) [H : is_contr A] : (Σa, B a) ≃ B (center A)
   :=
   equiv.mk _ (adjointify
-    (λu, (center_eq u.1)⁻¹ ▹ u.2)
+    (λu, (center_eq u.1)⁻¹ ▸ u.2)
     (λb, ⟨!center, b⟩)
-    (λb, ap (λx, x ▹ b) !hprop_eq_of_is_contr)
+    (λb, ap (λx, x ▸ b) !hprop_eq_of_is_contr)
     (λu, sigma_eq !center_eq !tr_inv_tr))
 
   /- Associativity -/
@@ -273,7 +273,7 @@ namespace sigma
   definition sigma_assoc_equiv (C : (Σa, B a) → Type) : (Σa b, C ⟨a, b⟩) ≃ (Σu, C u) :=
   equiv.mk _ (adjointify
     (λav, ⟨⟨av.1, av.2.1⟩, av.2.2⟩)
-    (λuc, ⟨uc.1.1, uc.1.2, !eta⁻¹ ▹ uc.2⟩)
+    (λuc, ⟨uc.1.1, uc.1.2, !eta⁻¹ ▸ uc.2⟩)
     begin intro uc, cases uc with u c, cases u, reflexivity end
     begin intro av, cases av with a v, cases v, reflexivity end)
 
@@ -281,7 +281,7 @@ namespace sigma
   definition assoc_equiv_prod (C : (A × A') → Type) : (Σa a', C (a,a')) ≃ (Σu, C u) :=
   equiv.mk _ (adjointify
     (λav, ⟨(av.1, av.2.1), av.2.2⟩)
-    (λuc, ⟨pr₁ (uc.1), pr₂ (uc.1), !prod.eta⁻¹ ▹ uc.2⟩)
+    (λuc, ⟨pr₁ (uc.1), pr₂ (uc.1), !prod.eta⁻¹ ▸ uc.2⟩)
     proof (λuc, destruct uc (λu, prod.destruct u (λa b c, idp))) qed
     proof (λav, destruct av (λa v, destruct v (λb c, idp))) qed)
 
@@ -376,8 +376,8 @@ namespace sigma
          apply IH,
            apply is_trunc.is_trunc_eq,
            intro p,
-             show is_trunc n (p ▹ u .2 = v .2), from
-             is_trunc.is_trunc_eq n (p ▹ u.2) (v.2),
+             show is_trunc n (p ▸ u .2 = v .2), from
+             is_trunc.is_trunc_eq n (p ▸ u.2) (v.2),
   end
 
 end sigma
diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean
index 5453554b2..b6a2627d9 100644
--- a/hott/types/trunc.hlean
+++ b/hott/types/trunc.hlean
@@ -121,7 +121,7 @@ namespace is_trunc
   @equiv_of_is_hprop _ _ _
     (@is_trunc_eq _ _ (is_hset_of_relation R mere refl @imp) a b)
     imp
-    (λp, p ▹ refl a)
+    (λp, p ▸ refl a)
 
   local attribute not [reducible]
   definition is_hset_of_double_neg_elim {A : Type} (H : Π(a b : A), ¬¬a = b → a = b)