[Agda] Preorder.setoid ?

[Sergei Meshveliani]

Dear Standard library developers,

lib-0.7  has  record Preorder  ...

1) Intuitively, a  Preorder  is also a  Setoid.
2) record Preorder  has all parts of Setoid.
3) Programmers would often like to extract  Setoid  from  Preorder
   (ToTalOrder, DecTotalOrder, ...). 

So, has it sense to add to  `record Preorder'   the lines   

  setoid : Setoid c ℓ₁  
  setoid = record{ Carrier       = Carrier  
                 ; _≈_           = _≈_ 
                 ; isEquivalence = isEquivalence } 
?

Regards,

------
Sergei