[Agda] Simple Agda Libraries

[James McKinna]

Thanks Wouter for this (admittedly retrograde) step.

As a very old-fashioned person, I nevertheless love the mixfixes in 
Agda, while loathing the Unicode, because ... I just have not learned to 
upgrade my typing style/my mental model of what keystrokes turn into 
what glyphs (and I am getting a bit old to learn a set of character 
tables/ \uxxxx escapes by rote, I reckon).

I know this isn't just old-fashionedness, but the ingrained Anglo 
cultural bias which ASCII and ASCII keyboards have left us with, and 
which it would be good to outgrow (I guess everyone else had previously 
to learn a lot of escape sequences and tables for Chinese and Japanese, 
bvb.).

As well as supporting Wouter's idea, could the Unicode experts offer 
some insight into how to migrate to using it effectively?

Apologies for the naivete of the question, but it is meant seriously.

James

Wouter Swierstra wrote:
> Dear all,
>
> I have to admit I'm a bit hesitant to use the standard libraries. It 
> has a bit too much Unicode mixfix madness for my taste. Call me 
> old-fashioned, but I quite like identifiers everyone immediately knows 
> how to type.
> ...