There's certainly many things that could be improved about Agda, but they mostly have to do with its semantics. Here's a great blog post about some of them: https://jesper.sikanda.be/posts/why-not-a-core-language.html

Operator fixity is a non-issue; if you don't like how the fixities have been set up, you can change them at will, even in the middle of an `import` statement. Nobody is making you use custom infix operators, either; you can write Agda that looks mostly like a Lisp if you wish.

Improving `with` is ongoing work; there was a presentation on it at the recent Agda implementors' meeting.

There's real people with real feelings building Agda, and not very many of them either. Consider that before publicly denigrating their work, with such shallow criticism to boot.

Yes, and I know some of them and have critiqued it in person.