[Agda] Preorder.setoid ?

[Nils Anders Danielsson]

On 2013-09-16 17:22, Sergei Meshveliani wrote:
> So, has it sense to add to  `record Preorder'   the lines
>
>    setoid : Setoid c ℓ₁
>    setoid = record{ Carrier       = Carrier
>                   ; _≈_           = _≈_
>                   ; isEquivalence = isEquivalence }
> ?

No, not in this way, because Setoid is defined after Preorder.

Note also that your definition uses the /underlying/ equivalence, not
the main preorder relation.

-- 
/NAD