Ok, that's neat. Is there a proof checker and an editor/IDE other than Emacs' Agda mode?

Because I'm probably going to stick with Coq for its tooling.