在Agda的标准库中，可以使用maximum函数来找到一个列表中的最大值。以下是一个包含代码示例的解决方法：

open import Agda.Builtin.Nat
open import Data.List
open import Data.Nat

maxList : List ℕ → ℕ
maxList [] = 0
maxList (x ∷ xs) = max x (maxList xs)

example : maxList [1, 5, 3, 8, 2] ≡ 8
example = refl

在这个例子中，我们首先引入了所需的Agda库模块，然后定义了一个名为maxList的函数。maxList函数接受一个List ℕ类型的参数，并返回一个ℕ类型的结果。在函数定义中，我们处理了两种情况：如果列表为空，则返回0；否则，我们使用max函数找到列表中的最大值，并递归调用maxList函数来处理剩余的列表。

最后，我们提供了一个名为example的例子来验证maxList函数的正确性。我们使用refl函数来证明maxList [1, 5, 3, 8, 2]的结果确实等于8。

请注意，这只是一个简单的示例，实际的Agda标准库可能提供更多复杂和高效的方法来处理列表的最大值。