One other difference between Idris and Agda is that Idris's propositional equality is heterogeneous, while Agda's is homogeneous.
In other words, the putative definition of equality in Idris would be:
data (=) : {a, b : Type} -> a -> b -> Type where
refl : x = x
while in Agda, it is
data _≡_ {l} {A : Set l} (x : A) : A → Set a where
refl : x ≡ x
The l in the Agda defintion can be ignored, as it has to do with the universe polymorphism that Edwin mentions in his answer.
The important difference is that the equality type in Agda takes two elements of A as arguments, while in Idris it can take two values with potentially different types.
In other words, in Idris one can claim that two things with different types are equal (even if it ends up being an unprovable claim), while in Agda, the very statement is nonsense.
This has important and wide-reaching consequences for the type theory, especially regarding the feasibility of working with homotopy type theory. For this, heterogeneous equality just won't work because it requires an axiom that is inconsistent with HoTT. On the other hand, it is possible to state useful theorems with heterogeneous equality that can't be straightforwardly stated with homogeneous equality.
Perhaps the easiest example is associativity of vector concatenation. Given length-indexed lists called vectors defined thusly:
data Vect : Nat -> Type -> Type where
Nil : Vect 0 a
(::) : a -> Vect n a -> Vect (S n) a
and concatenation with the following type:
(++) : Vect n a -> Vect m a -> Vect (n + m) a
we might want to prove that:
concatAssoc : (xs : Vect n a) -> (ys : Vect m a) -> (zs : Vect o a) ->
xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
This statement is nonsense under homogeneous equality, because the left side of the equality has type Vect (n + (m + o)) a and the right side has type Vect ((n + m) + o) a. It's a perfectly sensible statement with heterogeneous equality.
