[Agda] "No instance"

[Sergei Meshveliani]

Please, what it wrong here?

----------------------------------------------------------------------
open import Level using (suc; _⊔_)
open import Relation.Binary using (Rel; IsEquivalence; _Preserves_⟶_)
open import Data.Product using (Σ)

record Setoid {α} α= (Carrier : Set α) :  Set (suc (α ⊔ α=))  where
  infix 4 _≈_
  field
    _≈_           : Rel Carrier α=
    isEquivalence : IsEquivalence _≈_


module _ {α α= β β=} {C : Set α} {C' : Set β}
                     (S : Setoid α= C) (S' : Setoid β= C')
  where
  open Setoid {{...}}

  CongruentMap :  Set _
  CongruentMap =  Σ (C → C') (\f → f Preserves _≈_ ⟶ _≈_)
---------------------------------------------------------------

Agda 2.6.0-c5cbc7e :

"No instance of type Setoid _ℓ₁_29 C was found in scope.
when checking that the expression _≈_ has type Rel C _ℓ₁_29
"


Thanks,

------
Sergei