Agda is primarily a theorem prover, Idris doesn't try to compete with that. They're rather similar in a lot of ways, but Idris targets more general purpose programming. F* is more similar in its goals, but it kind of has its own paradigm. I think a lot of the focus behind F* was based on crypto applications, so it's a bit less general purpose. It also approaches I/O without monads (to my understanding, it just uses Tot, ML, etc. to mark effects for types). The syntax is more ML-like (not super important), but in terms of the type system it's very strange compared to Idris (it focuses on refinement types versus using things like GADTs to construct a lot of the primitives -- the F* way of creating nat is to assert that an integer is >= 0 instead of defining the natural number as Zero | Succ Nat).

Indeed. Idris aims to be "PacMan complete". As in it should be perfectly feasible to write PacMan using Idris.

From using Agda it is fairly similar since both do theorem proving by programming in a unified language vs Coq which has separate languages for programming and proving. Where Idris excels is a standard library focused on systems programming, things like good console input/output support that Agda doesn't focus on.

Idris & Agda are based on calculus of constructions

F* is based on type refinements and smt solver.

in theory all DT are equivalent but type refinements are less expressive in practice than CoC.

sometimes the smt solver gives up and you are in trouble.

alternatively the smt solver can provide simple refinements with less effort than CoC when it does work.

And ATS [3]?

[3] http://www.ats-lang.org/