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