[Agda] change in operator syntax

[Sergei Meshveliani]

People,
I am trying the  Development Agda of  August 13, 2015.

The attached code (25 nonempty lines) produces the report

-----------------
Don't know how to parse _~_ Respects2 _≈_. Could mean any one of:
  _Respects2_ _~_ _≈_
  _Respects2_ _~_ _≈_
  _Respects2_ _~_ _≈_
  _Respects2_ _~_ _≈_
Operators used in the grammar:
  Respects2  (infix operator, unrelated)           [_Respects2_ 
  ...
  ...
-----------------

What can be the matter about this?

Thanks,

------
Sergei

-------------- next part --------------
open import Level           using (_⊔_)
open import Relation.Binary using (Rel)
open import Data.Product    using (_×_)

infix 3 _←→_

_←→_ : ∀ {α β} (A : Set α) → (B : Set β) → Set (α ⊔ β)
_←→_ A B =  (A → B) × (B → A)

_Respects2_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} → Rel A ℓ₁ → Rel A ℓ₂ → Set _
_Respects2_ _~_ _≈_ =
                      ∀ {x x' y y'} → x ≈ x' → y ≈ y' → x ~ y → x' ~ y'

Respects₂gen : ∀ {α α= β β= ℓ} {A : Set α} {B : Set β} →
                               (A → B → Set ℓ) → Rel A α= → Rel B β= → Set _
Respects₂gen _~_ _~₁_ _~₂_ =
                         ∀ {x x' y y'} → x ~₁ x' → y ~₂ y' → x ~ y → x' ~ y'

Respects2←→Respects₂gen :
           ∀ {a ℓ₁ ℓ₂} {A : Set a} → (_~_ : Rel A ℓ₁) → (_≈_ : Rel A ℓ₂) →
                       ((_~_ Respects2 _≈_) ←→ (Respects₂gen _~_ _≈_ _≈_))

Respects2←→Respects₂gen {a} {ℓ₁} {ℓ₂} {A} _≈_ _~_ =
                                                  (to _≈_ _~_ , from _≈_ _~_)
  where
  to : (_~_ : Rel A ℓ₁) → (_≈_ : Rel A ℓ₂) → _~_ Respects2 _≈_ →
                                                 Respects₂gen _~_ _≈_ _≈_
  to _≈_ _~_ ~resp≈ x≈x' y≈y' x~y =  ~resp≈ x≈x' y≈y' x~y

  from : (_~_ : Rel A ℓ₁) → (_≈_ : Rel A ℓ₂) → Respects₂gen _~_ _≈_ _≈_ →
                                                            _~_ Respects2 _≈_
  from _~_ _≈_ ~resp'≈≈ x≈x' y≈y' x~y =  ~resp'≈≈ x≈x' y≈y' x~y