我认为这是一个非常好的方法。通常，当你想创建一个类型的“子集”时，它看起来像：
postulate
A : Set
P : A → Set
record Subset : Set where
field
value : A
prop : P value
但是，这可能不是一个子集，因为它实际上可以包含比原始类型更多的元素。那是因为prop可能有更多不同的价值。例如：
open import Data.Nat
data ℕ-prop : ℕ → Set where
c1 : ∀ n → ℕ-prop n
c2 : ∀ n → ℕ-prop n
record ℕ-Subset : Set where
field
value : ℕ
prop : ℕ-prop value
突然之间，子集的元素数量是原始类型的两倍。这个例子有点做作，我同意，但想象一下你在集合上有一个子集关系（来自集合论的集合）。这样的事情实际上是相当可能的：
sub₁ : {1, 2} ⊆ {1, 2, 3, 4}
sub₁ = drop 3 (drop 4 same)
sub₂ : {1, 2} ⊆ {1, 2, 3, 4}
sub₂ = drop 4 (drop 3 same)
解决这个问题的常用方法是使用不相关的参数：
record Subset : Set where
field
value : A
.prop : P value
这意味着如果两个类型Subset的值具有相同的value，则该prop字段与相等性无关。事实上：
record Subset : Set where
constructor sub
field
value : A
.prop : P value
prop-irr : ∀ {a b} {p : P a} {q : P b} →
a ≡ b → sub a p ≡ sub b q
prop-irr refl = refl
但是，这更像是一个指导方针，因为您的代表不受此问题的影响。这是因为在 Agda 中模式匹配的实现隐含了公理 K：
K : ∀ {a p} {A : Set a} (x : A) (P : x ≡ x → Set p) (h : x ≡ x) →
P refl → P h
K x P refl p = p
好吧，这并不能告诉你太多。幸运的是，还有另一个等价于公理 K 的性质：
uip : ∀ {a} {A : Set a} {x y : A} (p q : x ≡ y) → p ≡ q
uip refl refl = refl
这告诉我们只有一种方式可以使两个元素相等，即refl（uip表示身份证明的唯一性）。
这意味着当您使用命题相等来制作子集时，您将得到一个真正的子集。
让我们明确一点：
isSingleton : ∀ {ℓ} → Set ℓ → Set _
isSingleton A = Σ[ x ∈ A ] (∀ y → x ≡ y)
isSingleton A表示仅包含一个元素的事实A，直到命题相等。事实上，Singleton x是一个单例：
Singleton-isSingleton : ∀ {ℓ} {A : Set ℓ} (x : A) →
isSingleton (Singleton x)
Singleton-isSingleton x = (x , refl) , λ {(.x , refl) → refl}
有趣的是，这在没有公理 K 的情况下也可以工作。如果你把{-# OPTIONS --without-K #-}pragma 放在文件的顶部，它仍然可以编译。