diff --git a/hott/init/reserved_notation.hlean b/hott/init/reserved_notation.hlean
index 2207e12f8..acbc6c5e3 100644
--- a/hott/init/reserved_notation.hlean
+++ b/hott/init/reserved_notation.hlean
@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: init.reserved_notation
 Authors: Leonardo de Moura
 -/
-
 prelude
 import init.datatypes
 
@@ -18,11 +17,9 @@ notation `take`   binders `,` r:(scoped f, f) := r
   If a module reassigns these, it will be incompatible with other modules that adhere to these
   conventions.
 
-  When hovering over a symbol, use "C-u C-x =" to see how to input it.
+  When hovering over a symbol, use "C-c C-k" to see how to input it.
 -/
 
-/- Logical operations and relations -/
-
 definition std.prec.max   : num := 1024 -- the strength of application, identifiers, (, [, etc.
 definition std.prec.arrow : num := 25
 
@@ -37,22 +34,23 @@ num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (
 
 /- Logical operations and relations -/
 
-
 reserve prefix `¬`:40
 reserve prefix `~`:40
 reserve infixr `∧`:35
 reserve infixr `/\`:35
 reserve infixr `\/`:30
 reserve infixr `∨`:30
-reserve infix `<->`:25
-reserve infix `↔`:25
+reserve infix `<->`:20
+reserve infix `↔`:20
 reserve infix `=`:50
 reserve infix `≠`:50
 reserve infix `≈`:50
 reserve infix `∼`:50
+reserve infix `≡`:50
 
 reserve infixr `∘`:60                   -- input with \comp
 reserve postfix `⁻¹`:std.prec.max_plus  -- input with \sy or \-1 or \inv
+
 reserve infixl `⬝`:75
 reserve infixr `▸`:75
 
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index c393a6095..1e5025e5a 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -689,7 +689,7 @@ section port_algebra
     algebra.sub_add_eq_sub_sub_swap
   theorem sub_eq_iff_eq_add : ∀a b c : ℤ, a - b = c ↔ a = c + b := algebra.sub_eq_iff_eq_add
   theorem eq_sub_iff_add_eq : ∀a b c : ℤ, a = b - c ↔ a + c = b := algebra.eq_sub_iff_add_eq
-  theorem eq_iff_eq_of_sub_eq_sub : ∀{a b c d : ℤ}, a - b = c - d → a = b ↔ c = d :=
+  theorem eq_iff_eq_of_sub_eq_sub : ∀{a b c d : ℤ}, a - b = c - d → (a = b ↔ c = d) :=
     @algebra.eq_iff_eq_of_sub_eq_sub _ _
   theorem eq_sub_of_add_eq : ∀{a b c : ℤ}, a + c = b → a = b - c := @algebra.eq_sub_of_add_eq _ _
   theorem sub_eq_of_eq_add : ∀{a b c : ℤ}, a = c + b → a - b = c := @algebra.sub_eq_of_eq_add _ _
diff --git a/library/data/int/order.lean b/library/data/int/order.lean
index 498daab89..21f79368f 100644
--- a/library/data/int/order.lean
+++ b/library/data/int/order.lean
@@ -326,7 +326,7 @@ section port_algebra
   theorem add_neg_of_nonpos_of_neg : ∀{a b : ℤ}, a ≤ 0 → b < 0 → a + b < 0 :=
     @algebra.add_neg_of_nonpos_of_neg _ _
   theorem add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg : ∀{a b : ℤ},
-    0 ≤ a → 0 ≤ b → a + b = 0 ↔ a = 0 ∧ b = 0 :=
+    0 ≤ a → 0 ≤ b → (a + b = 0 ↔ a = 0 ∧ b = 0) :=
     @algebra.add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg _ _
 
   theorem le_add_of_nonneg_of_le : ∀{a b c : ℤ}, 0 ≤ a → b ≤ c → b ≤ a + c :=
@@ -416,9 +416,9 @@ section port_algebra
     algebra.lt_add_iff_sub_lt_left
   theorem lt_add_iff_sub_lt_right : ∀a b c : ℤ, a < b + c ↔ a - c < b :=
     algebra.lt_add_iff_sub_lt_right
-  theorem le_iff_le_of_sub_eq_sub : ∀{a b c d : ℤ}, a - b = c - d → a ≤ b ↔ c ≤ d :=
+  theorem le_iff_le_of_sub_eq_sub : ∀{a b c d : ℤ}, a - b = c - d → (a ≤ b ↔ c ≤ d) :=
     @algebra.le_iff_le_of_sub_eq_sub _ _
-  theorem lt_iff_lt_of_sub_eq_sub : ∀{a b c d : ℤ}, a - b = c - d → a < b ↔ c < d :=
+  theorem lt_iff_lt_of_sub_eq_sub : ∀{a b c d : ℤ}, a - b = c - d → (a < b ↔ c < d) :=
     @algebra.lt_iff_lt_of_sub_eq_sub _ _
   theorem sub_le_sub_left : ∀{a b : ℤ}, a ≤ b → ∀c : ℤ, c - b ≤ c - a :=
     @algebra.sub_le_sub_left _ _
diff --git a/library/init/quot.lean b/library/init/quot.lean
index bd16be1b6..e69eded61 100644
--- a/library/init/quot.lean
+++ b/library/init/quot.lean
@@ -13,7 +13,7 @@ open sigma.ops setoid
 
 constant quot.{l}   : Π {A : Type.{l}}, setoid A → Type.{l}
 -- Remark: if we do not use propext here, then we would need a quot.lift for propositions.
-constant propext {a b : Prop} : a ↔ b → a = b
+constant propext {a b : Prop} : (a ↔ b) → a = b
 
 namespace quot
   constant mk        : Π {A : Type}   [s : setoid A], A → quot s
diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean
index 010ab1c9b..8867ef0ac 100644
--- a/library/init/reserved_notation.lean
+++ b/library/init/reserved_notation.lean
@@ -17,7 +17,7 @@ notation `take`   binders `,` r:(scoped f, f) := r
   If a module reassigns these, it will be incompatible with other modules that adhere to these
   conventions.
 
-  When hovering over a symbol, use "C-u C-x =" to see how to input it.
+  When hovering over a symbol, use "C-c C-k" to see how to input it.
 -/
 
 definition std.prec.max   : num := 1024 -- the strength of application, identifiers, (, [, etc.
@@ -40,8 +40,8 @@ reserve infixr `∧`:35
 reserve infixr `/\`:35
 reserve infixr `\/`:30
 reserve infixr `∨`:30
-reserve infix `<->`:25
-reserve infix `↔`:25
+reserve infix `<->`:20
+reserve infix `↔`:20
 reserve infix `=`:50
 reserve infix `≠`:50
 reserve infix `≈`:50