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

[Andrés Sicard-Ramírez]

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} → ⊥ ⊎ T → T
f (inj₁ ())
f (inj₂ t) = t

-- 
Andrés