[Agda] Fairbairn not for St.lib

[Serge D. Mechveliani]

To my suggestion of 2012-10-11 of
> 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

Nils Anders Danielsson  responds

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


1. I do not insist on my particular suggestion with  project\bot\u+,
   I am a beginner in Agda.

2. But I think that, mainly and in general, 
   the Fairbairn threshold is not for Standard library
   ( if I have found a proper definition! ).

I `google' the definition somewhere in e-mail: 
--------
http://www.haskell.org/pipermail/libraries/2012-February/017548.html
Edward Kmett ekmett at gmail.com Feb 15 2012
[..]
The Fairbairn threshold is the point at which the effort of looking up or
keeping track of the definition is outweighed by the effort of rederiving
it or inlining it.
--------

If I confuse the definition, then I am very sorry!

My idea is as follows.
To detect whether a code is desirable for a Standard library, one needs
first to estimate aprroximately: 

  how many users  have programmed or are likely to program this map.  

I do not know what the Fairbairn threshold is for, but for the decision
on Standard library  the above measure is more important. 

Consider the example of the function
  null : forall {a} {A : Set a} -> List A -> Bool
  null []        = true
  null (x :: xs) = false

from the Agda Standard library lib-0.6.
Is it above the Fairbairn threshold? Probably, is not.
But I think:  it needs to be in the Standard library.

Because otherwise somewhat 50.000 users will write their own functions
for the same map, called  
    null, nullList, null?, isNull, nullList?, empty, empty?, emptyList, 
    nil, nil?, nilList ...  
-- there will appear about 10 names.
Also in many shortly written functions there are possible different 
signatures: arguments swapped, additional parameter, making an argument 
implicit, and so on.
This will make it somewhat 100 variants.

Now: these users would read each other programs much easier -- if they
look into Standard library, and replace their own variant with something
related to it in Standard.

Regards,
Sergei