[Agda] Preorder.setoid ?

[Sergei Meshveliani]

On Tue, 2013-09-17 at 10:04 +0200, Nils Anders Danielsson wrote:
> 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.
> 

All right, then, the same can be done for  Poset,  and inherited in
TotalOrder and such.


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

If you call  Preorder._≈_   underlying,   then yes, this was my
suggestion.

If you call  Preorder._~_   the main preorder relation,  then this
`setoid' cannot be set for this _~_.  Because there is not declared 
(and need not to be declared)  isEquivalence  for this  _~_.

Am I missing something?

Regards,

------
Sergei