How to define a singleton set?

Question 1

I think this is a very good way to do it. Usually, when you want to create a "subset" of a type, it looks like:

postulate
  A : Set
  P : A → Set

record Subset : Set where
  field
    value : A
    prop  : P value

However, this might not be a subset in the sense that it can actually contain more elements than the original type. That is because prop might have more propositionally different values. For example:

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

And suddenly, the subset has twice as many elements as the original type. This example is a bit contrived, I agree, but imagine you had a subset relation on sets (sets from set theory). Something like this is actually fairly possible:

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)

The usual approach to this problem is to use irrelevant arguments:

record Subset : Set where
  field
    value : A
    .prop : P value

This means that two values of type Subset are equal if they have the same value, the prop field is irrelevant to the equality. And indeed:

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

However, this is more of a guideline, because your representation doesn't suffer from this problem. This is because the implementation of pattern matching in Agda implies axiom 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

Well, this doesn't tell you much. Luckily, there's another property that is equivalent to axiom K:

uip : ∀ {a} {A : Set a} {x y : A} (p q : x ≡ y) → p ≡ q
uip refl refl = refl

This tells us that there's only one way in which two elements can be equal, namely refl (uip means uniqueness of identity proofs).

This means that when you use propositional equality to make a subset, you're getting a true subset.

Let's make this explicit:

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

isSingleton A expresses the fact that A contains only one element, up to propositonal equality. And indeed, Singleton x is a singleton:

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

Interestingly, this also works without axiom K. If you put {-# OPTIONS --without-K #-} pragma at the top of your file, it will still compile.

Question 2

You can define a record without projections:

record Singleton {α} {A : Set α} (x : A) : Set α where

fromSingleton : ∀ {α} {A : Set α} {x : A} -> Singleton x -> A
fromSingleton {x = x} _ = x

singleton : ∀ {α} {A : Set α} -> (x : A) -> Singleton x
singleton _ = _

Or equalently

record Singleton {α} {A : Set α} (x : A) : Set α where

  fromSingleton = x
open Singleton public

singleton : ∀ {α} {A : Set α} -> (x : A) -> Singleton x
singleton _ = _

Now you can use it like this:

open import Relation.Binary.PropositionalEquality
open import Data.Nat

f : Singleton 5 -> ℕ
f x = fromSingleton x

test : f (singleton 5) ≡ 5
test = refl

test' : f _ ≡ 5
test' = refl

And this is rejected:

fail : f (singleton 4) ≡ 4
fail = ?

The error:

4 != 5 of type ℕ
when checking that the expression singleton 4 has type Singleton 5

Question 3

It can be defined as an indexed datatype:

data Singleton {ℓ : _} {A : Set ℓ} : A -> Set where
  singleton : (a : A) -> Singleton a

This is analogous to how propositional equality a ≡ b is indexed by two particular elements a and b, or how Vector X n is indexed by a particular n ∈ ℕ.