Haskell Deriving Mechanism for Agda
<p>I am wondering if there is anything in Agda that resembles Haskell's <code>deriving Eq</code> clause ---then I have an associated question below, as well.</p>

<p>For example, suppose I have types for a toy-language,</p>

<pre><code>data Type : Set where
  Nat  : Type
  Prp : Type
</code></pre>

<p>Then I can implement decidable equality by pattern matching and <code>C-c C-a</code>,</p>

<pre><code>_≟ₜ_ : Decidable {A = Type} _≡_
Nat ≟ₜ Nat = yes refl
Nat ≟ₜ Prp = no (λ ())
Prp ≟ₜ Nat = no (λ ())
Prp ≟ₜ Prp = yes refl
</code></pre>

<p>I'm curious if this can be mechanised or automated somehow similar to the manner it is done in Haskell:</p>

<pre><code>data Type = Nat | Prp deriving Eq
</code></pre>

<p>Thank-you!</p>

<p>While we're on the topic of types, I'd like to realise my formal types as Agda types: Nat is just natural numbers while Prp is small propositions.</p>

<pre><code>⟦_⟧Type : Type → Set ?
⟦ Nat ⟧Type = ℕ
⟦ Prp ⟧Type = Set
</code></pre>

<p>Sadly this does not work. I tried to fix this with lifting but failed since I haven't a clue on how to use level lifting. Any help is appreciated!</p>

<p>An example usage of the above function would be,</p>

<pre><code>record InterpretedFunctionSymbol : Set where
  field
   arity   : ℕ
   src tgt : Type
   reify   : Vec ⟦ src ⟧Type arity → ⟦ tgt ⟧Type
</code></pre>

<p>Thank-you for humouring me!</p>