在Agda中，可以通过定义导数类型来表示数据结构的导数。导数类型是原始数据结构中的每个构造子的类型，其中构造子的参数被替换为它们的导数类型。

以下是一个示例，展示如何使用导数类型来表示自然数的导数：

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

data ℕ′ : Set where
  zero′ : ℕ′
  succ′ : ℕ′ → ℕ′

data ℕ′′ : Set where
  zero′′ : ℕ′′
  succ′′ : ℕ′′ → ℕ′′

data ℕ′′′ : Set where
  zero′′′ : ℕ′′′
  succ′′′ : ℕ′′′ → ℕ′′′

data ℕ′′′′ : Set where
  zero′′′′ : ℕ′′′′
  succ′′′′ : ℕ′′′′ → ℕ′′′′

data ℕ′′′′′ : Set where
  zero′′′′′ : ℕ′′′′′
  succ′′′′′ : ℕ′′′′′ → ℕ′′′′′

在上面的例子中，我们定义了自然数的6个导数类型：ℕ′、ℕ′′、ℕ′′′、ℕ′′′′和ℕ′′′′′。每个导数类型对应于原始数据结构中的每个构造子，其中构造子的参数被替换为它们的导数类型。

现在，我们可以使用这些导数类型来定义操作，例如加法运算：

_+_ : ℕ → ℕ → ℕ
zero + n = n
succ m + n = succ (m + n)

_+′ : ℕ′ → ℕ′ → ℕ′
zero′ +′ n = n
succ′ m +′ n = succ′ (m +′ n)

_+′′ : ℕ′′ → ℕ′′ → ℕ′′
zero′′ +′′ n = n
succ′′ m +′′ n = succ′′ (m +′′ n)

_+′′′ : ℕ′′′ → ℕ′′′ → ℕ′′′
zero′′′ +′′′ n = n
succ′′′ m +′′′ n = succ′′′ (m +′′