agda - 如何定义单例集？

Question

假设我有一个值 x : A 并且我想定义一个只包含 x 的集合。

这是我尝试过的:

open import Data.Product
open import Relation.Binary.PropositionalEquality

-- Singleton x is the set that only contains x. Its values are tuples containing
-- a value of type A and a proof that this value is equal to x.
Singleton : ∀ {ℓ} {A : Set ℓ} → (x : A) → Set ℓ
Singleton {A = A} x = Σ[ y ∈ A ] (y ≡ x)

-- injection
singleton : ∀ {ℓ} {A : Set ℓ} → (x : A) → Singleton x
singleton x = x , refl

-- projection
fromSingleton : ∀ {ℓ} {A : Set ℓ} {x : A} → Singleton x → A
fromSingleton s = proj₁ s

有更好的方法吗？

---

我为什么要这个的一个例子:如果你有一个幺半群在某个集合 A 上，那么你可以形成一个以 A 作为唯一对象的类别。要在 Agda 中表达这一点，您需要一种方法来编写“仅包含 A 的集合”。

Answer 1

我认为这是一个很好的方法。通常，当你想创建一个类型的“子集”时，它看起来像:

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 放在文件顶部，它仍会编译。