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

[Daniel Peebles]

I think I've suggested this before, but there's super hyperlinked
documentation online at
http://www.cse.chalmers.se/~nad/listings/lib/Everything.html#1, so if you
navigate to a module that references something you don't know, you'll be
able to click on symbols you don't recognize (like \u+) and it will take
you to their definitions.

Another option to search is simply to type \u+ into Agda-mode, take the
symbol it gives you, paste that into grep, and grep anyway.

On Wed, Oct 10, 2012 at 11:59 AM, Serge D. Mechveliani <mechvel at botik.ru>wrote:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121010/b6d6003e/attachment-0001.html