Unicode is anathema if you're a working touch typist. It's a pity Agda developers obviously aren't.