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

[Serge D. Mechveliani]

On Thu, Oct 11, 2012 at 10:46:04AM -0500, Andr??s Sicard-Ram??rez wrote:
> On Thu, Oct 11, 2012 at 10:18 AM, Serge D. Mechveliani <mechvel at botik.ru> wrote:
> >
> > Further, it is clear to us that for any set T we can define a map
> >                                                  f : Empty \u+ T -> T
> > If any such  f  is defined for  T = (y <= x),  then  f v  is the goal.
> > But I fail to define such  f  in Agda !
> 
> f : {T : Set} -> \bot \u+ T -> T
> f (inj_1 ())
> f (inj_2 t) = t

(I have changed the math symbols -- SM).

Great! 
I have just missed a syntactic possibility of  f (inj_1 ()).

I do not know, may be, it worths adding to  Data.Sum  of Standard 
library the function 
  project\bot\u+ : {l : Level} -> {A : Set l} -> \bot \u+ A -> A
  project\bot\u+ (inj_1 ())
  project\bot\u+ (inj_2 a ) = a

Thanks,
Sergei