[Agda] comparing performance to Coq

[mechvel at scico.botik.ru]

People,

has anybody compared the performance of the Agda programs for ordinary 
computation
(without proofs) to similar programs in Coq (in Gallina langage?) ?
I mean Agda 2.6.1 + MAlonzo.

For example:

f : List Nat -> Bool
f xs = let rs  = reverse xs
            ys  = sortByInsert xs
            ys' = sortByInsert rs
            zs  = sortByMerge  xs
            zs' = sortByMerge  rs
        in
        ys =?= ys'  and  ys =?= zs  and  ys =?= zs'

For example, xs = [1 .. 1000].
Or maybe, other examples.

Thanks,

------
Sergei