At the Agda headquaters:

“OK, guys, so our user pool consists only of folks who already know Haskell and Emacs Is there a way to narrow it down more?”

“I got it, what if we allow unicode, so they also have to also know Latex ?”

“Brilliant!”