fixes agda#2400: use explicit quantification

src/Function/Relation/Binary/Setoid/Equality.agda

@@ -24,16 +24,16 @@ private
 
 infix 4 _≈_
 _≈_ : (f g : Func From To) → Set (a₁ ⊔ b₂)
-f ≈ g = {x : From.Carrier} → f ⟨$⟩ x To.≈ g ⟨$⟩ x
+f ≈ g = ∀ x → f ⟨$⟩ x To.≈ g ⟨$⟩ x
 
 refl : Reflexive _≈_
-refl = To.refl
+refl _ = To.refl
 
 sym : Symmetric _≈_
-sym = λ f≈g → To.sym f≈g
+sym f≈g x = To.sym (f≈g x)
 
 trans : Transitive _≈_
-trans = λ f≈g g≈h → To.trans f≈g g≈h
+trans f≈g g≈h x = To.trans (f≈g x) (g≈h x)
 
 isEquivalence : IsEquivalence _≈_
 isEquivalence = record  -- need to η-expand else Agda gets confused