[Agda] Total: x !<= y ==> y <= x

Serge D. Mechveliani mechvel at botik.ru
Wed Oct 10 17:59:28 CEST 2012

```People,
I have a beginner question on usage of DecTotalOrder of Standard
library.

I have  ord : DecTotalOrder,
_<=_  extracted from this  ord,
``with  x <=? y''   produced    no x-!<=-y
(I think,   x-!<=-y :  \neg x <= y )

(here I replace \<= with <= ).

And from this   x-!<=-y,  I need to construct  y<=x : y <= x.
Because I think that this a constructive reifation for a classical
lemma for  (Total <=)  of that   not (x <= y)  ==>  y <= x.
I see in  Relation.Binary, Core:

record IsTotalOrder ...
isPartialOrder : IsPartialOrder _~~_ _<=_
total          : Total _<=_

(here I replace some math symbols)

Total : forall {a l} {A : Set a} -> Rel A l -> Set _
Total _~_ = forall x y -> (x ~ y) \u+ (y ~ x)

, where  \u+  denotes, I think, something close to union of types.
How to operate with a data from  (P \u+ Q) ?
what are the constructors?
Probably, one needs to apply   total <= x y :  (x <= y) \u+ (y <= x)
and then to use                x-!<=-y :  \neg x <= y

Where  \u+  is defined in the Standard library?
It is visible a certain `combinator'  <\u+>,  with the denotation
[ P , Q ].  I do not know of what does all this mean.

If it was not a math symbol, I could apply  grep foo *.agda.

May be, Standard Library provides somewhere a lemma, like

(\neg x <= y) includedInto (y <= x)   for  _<=_  from  TotalOrder ?

Thank you in advance for explanation,

------
Sergei
```