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.