[Agda] Re: extending setoid

[Sergei Meshveliani]

Nils  wrote

On 2013-08-07 10:37, Sergei Meshveliani wrote:
>> mapSetoid : {c l l' : Level} → (A : Setoid c l) → (Y : Set l') →
>>                                      (Y → Setoid.Carrier A) → Setoid l' l
>> mapSetoid {c} {l} {l'} A Y f =  ...

> There is something like this in Relation.Binary.On.
>
> -- 
> /NAD


Indeed, I see in  Data.Relation.Binary.On :

  setoid : ∀ {s₁ s₂ b} {B : Set b} (S : Setoid s₁ s₂) →
           (B → Setoid.Carrier S) → Setoid _ _,

and also other useful `on' `functors'. This looks good.
Using this, my code becomes

  cardSetoid : Setoid _ _ 
  cardSetoid = On.setoid (Mb.setoid natSetoid) f
               where
               f : Cardinality → Maybe ℕ
               f (fin n)  = just n
               f infinity = nothing

But I do not understand some code details in  ...Binary.On.

1.
  setoid S f = record
    { isEquivalence = isEquivalence f (Setoid.isEquivalence S) }

1.1. It must return a value of the type  Setoid _ _.
And where are the values for the fields  Carrier  and  _≈_ ?
What is the mechanism for filling them in automatically?

1.2. This  ``= isEquivalence f (Setoid.isEquivalence S)''

probably, takes  isEquivalence  from the preceeding parameterized

  module _ {a b} {A : Set a} {B : Set b} (f : B → A) where ...

Is this so?
And the file does not contain any words `open' or `public',
and the  setoid  function  is out of the module  `_'.

Now, to use a function  foo  from this anonymous parameterized 
module, does one need to call 

             foo < parameter values for the module > 
                 < proper argument values for  _.foo >
?

Thank you in advance for explanation,

------
Sergei