Certified cost bounds in Agda: A step towards automated complexity analysis