[Agda] Fairbairn not for St.lib

[Wolfram Kahl]

On Sat, Oct 13, 2012 at 04:47:54PM +0400, Serge D. Mechveliani wrote:
> 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.

As a separate function with pattern matching, it certainly is above,
I would say...

However, from later the referenced message of Fairbairn:

 | Certainly complicated enough constructions deserve library
 | entries, and I admit I don't know where the break even point
 | is, but I'm pretty sure it comes above two words and some
 | punctuation -- unless it's something fundamental like
 | composition.

In this case, the ``two words and some punctuation''
would be

 [ \bot-elim , id ]'

(with

open import Function    using ( id )
open import Data.Empty  using ( \bot-elim )
open import Data.Sum    using ( [_,_]' )  -- ' is really \'1

)

The fact that Data.Sum does not already depend on Data.Empty
is, in my eyes, an additional argument against including
project\bot\u+ inside Data.Sum.


Wolfram