我是 Agda 的新手，我正在尝试定义一个prod类型的常量：
Z → (Z → ((Z → Set) → Set))
现在，我编写了以下 Agda 代码：
data Prod (X : Set) : ℕ → X where
prod : ℕ → (ℕ → ((ℕ → X) → X))
当我对它进行类型检查时，agda 会产生以下错误消息：
X != Set (_33 X_) of type Set
when checking the definition of Prod
非常感谢任何帮助