[Agda] Respects2 in IsPreorder is derivable

[Nils Anders Danielsson]

On 2010-02-21 19:53, kahl at cas.mcmaster.ca wrote:
> Is there a particular reason why IsPreorder in
> the standard library module Relation.Binary
> includes  ∼-resp-≈  as a field,
> although it is easily derivable from the other fields?

No. Thanks for spotting this. I have updated the definition of
IsPreorder.

--
/NAD