[Agda] _<=_ and _<_

[Sergei Meshveliani]

On Tue, 2013-09-24 at 17:18 +0400, Sergei Meshveliani wrote:

> [] 
> 2. For  Nat,  
>    it is natural to derive (I) and (II) from  DecTotalOrder,
>    as a specialization of the above generic laws. 
> 
> But  DecTotalOrder  says nothing about  _<_.
> Then, we are forced to derive (I) and (II) from the union of
> DecTotalOrder and StrictTotalOrder.
> Right?
> 
> Well,  Data.Nat  has  decTotalOrder.  But it is silent about 
> Strict(Total)Order.
> 
> What is the way out?
> The approach  "prove (I) and (II) individually for  Nat" 
> will cause individual proofs for  Integer, Nat × Nat, List Nat,
> and so on.
> 
> 
> 3. Consider the Order organization that follows literally the usual
> formula "less or equal".
> 
> (A) Having _≈_ and _<_,   _≤_ needs to be defined 
>                               (implemented) immediately
> Or
> (B) Having _≈_ and _≤_,   _<_ needs to be defined immediately.
> 
> Because this is natural.


But I see now  Relation.Binary.StrictToNonStrict

which defines     x ≤ y = (x < y) ⊎ (x ≈ y)

I hope this will do of what I asked for.
If so, then I am sorry for the noise.

Regards,

------
Sergei