Fix type for ≡-syntax in heterogeneous equality (#2494)

* fix type for ≡-syntax in heterogeneous equality

* make ≡-syntax level polymorphic for heterogeneous equality

* update CHANGELOG

* move the entry in CHANGELOG to bug-fixes

CHANGELOG.md

@@ -11,6 +11,10 @@ Bug-fixes
 
 * Removed unnecessary parameter `#-trans : Transitive _#_` from
   `Relation.Binary.Reasoning.Base.Apartness`.
+* Relax the types for `≡-syntax` in `Relation.Binary.HeterogeneousEquality`.
+  These operators are used for equational reasoning of heterogeneous equality
+  `x ≅ y`, but previously the three operators in `≡-syntax` unnecessarily require
+  `x` and `y` to have the same type, making them unusable in most situations.
 
 Non-backwards compatible changes
 --------------------------------

src/Relation/Binary/HeterogeneousEquality.agda

@@ -234,22 +234,22 @@ module ≅-Reasoning where
 
   infix 4 _IsRelatedTo_
 
-  data _IsRelatedTo_ {A : Set ℓ} {B : Set ℓ} (x : A) (y : B) : Set ℓ where
+  data _IsRelatedTo_ {A : Set a} {B : Set b} (x : A) (y : B) : Set a where
     relTo : (x≅y : x ≅ y) → x IsRelatedTo y
 
   start : ∀ {x : A} {y : B} → x IsRelatedTo y → x ≅ y
   start (relTo x≅y) = x≅y
 
-  ≡-go : ∀ {A : Set a} → Trans {A = A} {C = A} _≡_ _IsRelatedTo_ _IsRelatedTo_
+  ≡-go : ∀ {A : Set a} {B : Set b} → Trans {A = A} {C = B} _≡_ _IsRelatedTo_ _IsRelatedTo_
   ≡-go x≡y (relTo y≅z) = relTo (trans (reflexive x≡y) y≅z)
 
   -- Combinators with one heterogeneous relation
-  module _ {A : Set ℓ} {B : Set ℓ} where
+  module _ {A : Set a} {B : Set b} where
     open begin-syntax (_IsRelatedTo_ {A = A} {B}) start public
+    open ≡-syntax (_IsRelatedTo_ {A = A} {B}) ≡-go public
 
   -- Combinators with homogeneous relations
-  module _ {A : Set ℓ} where
-    open ≡-syntax (_IsRelatedTo_ {A = A}) ≡-go public
+  module _ {A : Set a} where
     open end-syntax (_IsRelatedTo_ {A = A}) (relTo refl) public
 
   -- Can't create syntax in the standard `Syntax` module for