[Agda] Re: extending setoid

[Nils Anders Danielsson]

On 2013-08-08 16:50, Sergei Meshveliani wrote:
> 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?

Unification (as if you had written _).

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

For information about "module _", see the release notes for Agda 2.3.2.

-- 
/NAD