They probably are already. (In Haskell, they would be by default. I don't know enough about Agda.)

That is indeed the case. In Agda, the default is call-by-name, which means that functions are applied before arguments are evaluated. This does not, however, include sharing, so evaluating

    (λ x → x + x) (fib 2000)

will evaluate `fib 2000` twice. Agda programs can also be compiled to Haskell, in which case they would have Haskell's evaluation strategy, which is generally call-by-need (and so would share the result of fib 2000 above.)

I've never been aware of whether Agda is CBN or CBV because it actually doesn't matter (!).

In a pure, terminating language like Agda evaluation is "confluent" which means that CBV and CBN evaluations are identical.

Identical up to one algorithm taking a few seconds, and another taking as long as the universe has been alive :)

Who runs Agda code anyway? :)

Not only CBV and CBN, but also strict evaluation.

Huh, for some reason I assumed that we were talking about Idris. I didn't read the post well enough.