[Agda] overloading operations

[Sergei Meshveliani]

Can anybody, please, explain how to arrange operation overloading
(something like classes) ?

The first example is

----------------------------------------------------------------
open import Level           using (_⊔_)
open import Relation.Binary using (Setoid)

module _ {α α= β β=} (A : Setoid α α=) (B : Setoid β β=)
  where
  open Setoid   -- {{...}}

  C  = Setoid.Carrier A
  C' = Setoid.Carrier B

  IsCongruent :  (C → C') → Set _
  IsCongruent f =
                {x y : C} → _≈_ A x y → _≈_ B (f x) (f y)    -- (I)

             -- {x y : C} → x ≈ y → (f x) ≈ (f y)            -- (II)

----------------------------------------------------------------


The line (I) does work.
Then I try the line (II), with un-commenting {{...}}. 
And it is not type-checked.
I hoped for that it would find that the first ≈ is on C, while the
second ≈ is on C'. But it does not.

And real examples are like this:

-----------------------------------------------------------------------
module _ {α α= β β=} (G : Group α α=) (G' : Group β β=)
 where
 ... 
 homomorphismPreservesInversion :
   (mHomo : MonoidHomomorphism)
   (let f = MonoidHomomorphism.carryMap mHomo) (x : C) →
                                               f (x ⁻¹) ≈' (f x) ⁻¹'
 homomorphismPreservesInversion
                (monoidHomo ((f , f-cong) , f∙homo) f-preserves-ε) x =
   begin≈'
     f x'                     ≈'[ ≈'sym (∙ε' fx') ]
     fx' ∙' ε'                ≈'[ ∙'cong2 (≈'sym (x∙'x⁻¹ fx)) ]
     fx' ∙' (fx ∙' fx ⁻¹')    ≈'[ ≈'sym (≈'assoc fx' fx (fx ⁻¹')) ]
     (fx' ∙' fx) ∙' fx ⁻¹'    ≈'[ ∙'cong1 (≈'sym (f∙homo x' x)) ]
     f (x' ∙ x) ∙' fx ⁻¹'     ≈'[ ∙'cong1 (f-cong (x⁻¹∙x x)) ]
     f ε ∙' fx ⁻¹'            ≈'[ ∙'cong1 f-preserves-ε ]
     ε' ∙' fx ⁻¹'             ≈'[ ε'∙ (fx ⁻¹') ]
     (f x) ⁻¹'
   end≈'
   where
   x' = x ⁻¹;   fx = f x;   fx' = f x'
----------------------------------------------------------------------

Here the carriers of G and G' are C and C',
≈ is on C,  ≈' is on C' (by renaming),  
_∙_ on C, _∙'_ on C',
ε is of G, ε' of G',  
_⁻¹ is of G,  _⁻¹' of G',
and so on.

It is desirable to make the code more readable by canceling some of the
above renaming. For example, to replace ε' with ε and _∙'_ with _∙_.
Is it possible to do this by using something like 
open Group {{...}}
?

Thanks,

------
Sergei