如何在Agda中证明严格自然数不等式的非自反性

我正在完成PLFA教材《Negation》章节的推荐习题，题目要求：利用否定证明严格不等式具有非自反性，即不存在自然数n使得n < n成立。

严格不等式的定义 #

data _<_ : ℕ → ℕ → Set where

    z<s : ∀ {n : ℕ}
        ------------
      → zero < suc n

    s<s : ∀ {m n : ℕ}
      → m < n
        -------------
      → suc m < suc n

我给出的非自反性定义 #

<-irreflexive : ∀ {n : ℕ} → n < n → ⊥
<-irreflexive n<n = ?

遇到的问题与疑问 #

• 我知道需要在右侧构造⊥，尝试使用¬但编译器报错提示“n<n : (n < n) !=< Set”。
• 想咨询：
  1. n<n的类型是什么？
  2. 我的解题方向是否正确？
  3. 相关解题提示。

内容的提问来源于stack exchange，提问作者Jackson