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

Nils Anders Danielsson nad at chalmers.se
Fri Oct 12 13:33:11 CEST 2012


On 2012-10-11 18:51, Serge D. Mechveliani wrote:
> 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

No, I don't think this function is above the Fairbairn threshold.

-- 
/NAD


More information about the Agda mailing list