3

値が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 だけを含む集合」と書く方法が必要です。

4

3 に答える 3

4

これはとても良い方法だと思います。通常、タイプの「サブセット」を作成する場合は、次のようになります。

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

そして突然、サブセットには元の型の 2 倍の要素があります。この例は少し不自然ですが、集合 (集合論からの集合) に部分集合関係があると想像してください。このようなことは、実際にはかなり可能です。

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

これは、タイプの 2 つの値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

これは、2 つの要素が等しくなる方法が 1 つしかないことを示しreflていuipます。

これは、命題等価性を使用してサブセットを作成すると、真のサブセットが得られることを意味します。

これを明示的にしましょう:

isSingleton : ∀ {ℓ} → Set ℓ → Set _
isSingleton A = Σ[ x ∈ A ] (∀ y → x ≡ y)

isSingleton AAは、命題的等価性まで、1 つの要素のみを含む事実を表します。そして確かにSingleton x、シングルトンです：

Singleton-isSingleton : ∀ {ℓ} {A : Set ℓ} (x : A) →
  isSingleton (Singleton x)
Singleton-isSingleton x = (x , refl) , λ {(.x , refl) → refl}

興味深いことに、これは公理 K がなくても機能します。{-# OPTIONS --without-K #-}プラグマをファイルの先頭に置くと、コンパイルされます。

于 2014-01-25T23:01:21.013 に答える