我正在关注Agda中的Haskell逻辑，数学和编程之路。该书指出：
空集是平凡的关系，并且是两个集合A和B之间的最小关系
在阿格达：
data ∅ : Set where
record ⊤ : Set where
record Σ (A : Set) (B : A → Set) : Set₁ where
constructor _,_
field
π₁ : A
π₂ : B π₁
_×_ : Set → Set → Set₁
A × B = Σ A (λ _ → B)
infixr 5 _×_ _,_
Relation : Set → Set₁
Relation P = P × P → Set
这样，我可以在特定集合上定义关系：
lteℕ : Relation ℕ
lteℕ(x , y) = x ≤ℕ y where
_≤ℕ_ : ℕ → ℕ → Set
O ≤ℕ O = ⊤
O ≤ℕ S y = ⊤
S x ≤ℕ O = ∅
S x ≤ℕ S y = x ≤ℕ y
infixr 5 _≤ℕ_
但是现在我有一个问题，因为空集关系的签名：
Set₁ != Set when checking that the expression Set has type Set，也会导致错误Ø : Relation Set。是否有办法在逻辑上仍然一致？谢谢！
答案取决于您所说的集合。如果用集合表示数学集合的表示形式（例如列表），则空集合仅由空列表表示。
如果设置的意思是表示类型的Agda Set，则答案要复杂一些：没有an空类型，但是您可以想到的数量很多的。更准确地说，您没有提供任何构造函数的空类型与数据类型一样多。那么问题就更多是“ 我选择哪种类型的空集？，而不是“ 我如何建模空集？”。
这里是一个强调此方面的agda模块的示例：首先，我有一些导入内容和模块的标题：
open import Agda.Primitive
open import Data.Nat hiding (_⊔_)
module EmptySets where
然后我从一个空类型开始，您可以想到的更简单：
data Empty : Set where
根据这种数据类型，可以写一个消除符：
Empty-elim : ∀ {a} {A : Set a} → Empty → A
Empty-elim ()
这基本上说，只要Empty成立，任何事物都成立。
但是，我还可以通过定义一系列类型为空的都是全关系的空集来将空集表示为空关系。首先，需要定义关系（我从标准库中获取了定义）：
REL : ∀ {a b} → Set a → Set b → (ℓ : Level) → Set (a ⊔ b ⊔ lsuc ℓ)
REL A B ℓ = A → B → Set ℓ
然后可以定义空关系家族：
data EmptyRelation {a b ℓ} {A : Set a} {B : Set b} : REL A B ℓ where
由于所有这些类型都是空的，它们都还提供了消除符：
EmptyRelation-elim : ∀ {a b x ℓ} {A : Set a} {B : Set b} {X : Set x} {u : A} {v : B} → EmptyRelation {ℓ = ℓ} u v → X
EmptyRelation-elim ()
因此，可以实例化此泛型类型以获取特定的空类型，例如，自然数上的空关系，这永远不成立：
EmptyNaturalRelation : REL ℕ ℕ lzero
EmptyNaturalRelation = EmptyRelation
这就是书中所解释的：由于一个关系是一对对的集合，因此空类型是该关系中最小的：其中没有对的那个类型。
但是您也可以使用谓词代替关系，说空集是给定类型上最小的谓词：一个永不成立的谓词，在这种情况下，表示为以下形式：
Pred : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ lsuc ℓ)
Pred A ℓ = A → Set ℓ
data EmptyPredicate {a ℓ} {A : Set a} : Pred A ℓ where
您甚至可能更疯狂，并决定按以下方式对空集进行建模：
data EmptySomething {a} {A B C D E Z : Set a} : A → B → C → D → E → Z → Set where
总而言之，agda中没有空集，但是空类型有潜在的无限性。
关于您在问题中显示的代码，存在一些错误：
为什么要创建两个空类型？您的第二个类型不应该代表逻辑上的true，在这种情况下，它应该具有一个没有参数的构造函数，通常称为tt
关系通常是在两个参数上定义的，而不是在成对的参数上定义的，然后，如果需要使它们以一对作为参数，则可以对其进行咖喱处理。
为什么要使lteℕ依赖于_≤ℕ_而不直接定义它？
您应该将lteℕ定义为数据类型，而不是返回自下而上的函数，这将使您将来可以对此词进行大小写分割。通常，这是通过这种方式定义的（在标准库中）：
data _≤_ : Rel ℕ 0ℓ where
z≤n : ∀ {n} → zero ≤ n
s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n