[Agda] Implicit vs. explicit function types

[Roly Perera]

Hi,

I've been using Agda for a couple of weeks and really enjoying it.
I'm now stuck understanding an error message which complains that (of
two function types) "one is an implicit function type and the other is
an explicit function type".

The code below repeats it.  I'm sure it's something very basic that
I'm missing but I'd really appreciate some help.  The problem is with
the type of the pair f , g.

many thanks,
Roly


open import Data.Product
open import Relation.Binary
open import Relation.Binary.Core

postulate
  World : Set
  _≤_ : Rel World

≤-resp-≡ : _≤_ Respects₂ _≡_
≤-resp-≡ = f , g where
  f : ∀ {w₁ w₂ w₃} → w₂ ≡ w₃ → w₁ ≤ w₂ → w₁ ≤ w₃
  f {w} {w′} .{w′} refl w≤w′ = w≤w′
  g : ∀ {w₁ w₂ w₃} → w₂ ≡ w₃ → w₂ ≤ w₁ → w₃ ≤ w₁
  g {w} {w′} .{w′} refl w′≤w = w′≤w