[Agda] _<=_ and _<_

[Sergei Meshveliani]

People, I have a couple of questions about general relation between 
                                                            _≤_ and _<_ 
in the  lib-0.7 standard library.

1. What is the most general situation in  lib-0.7  under which these
usual properties can be proved:
                                       
                       x ≤ y  iff  x < y ⊎ x ≈ y               (I),
                       x < y  ->  ¬ y ≤ x                      (II)
?

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.

Let us follow (A):

  record IsPartialOrder {a ℓ₁ ℓ₂} {A : Set a}
                        (_≈_ : Rel A ℓ₁) (_<_ : Rel A ℓ₂) :
                        Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      isPreorder : IsPreorder _≈_ _<_   
                                   -- redefine IsPreorder respectively
      antisym    : Antisymmetric _≈_ _<_

    _≤_ : Rel A ℓ₂
    x ≤ y =  x < y ⊎ x ≈ y

Of course, the axioms need to be corrected slightly.
And  StrictPartialOrder  will not need to introduce  _<_  as something
independent on  _≤_.

I suspect that if the  Ordering library part  is reorganized this way,
then using orderings will become easier.

Am I missing something? What is your opinion?

Regards,

------
Sergei