module Sets.Sigma where

Import list

open import Data.Bool using (Bool; true; false; if_then_else_)
open import Data.Empty using (⊥)
open import Data.Fin using (Fin; zero; suc)
open import Data.List using (List; []; _∷_; _++_)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Nat using (ℕ; zero; suc; _<_; s≤s; z≤n)
open import Data.Unit using (⊤; tt)
open import Data.Product using (_×_; _,_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
open import Data.Empty using (⊥)

Dependent pair

The generalization of _×_ is called Σ (Sigma) or dependent pair:

data Σ (A : Set) (B : A → Set) : Set where
  _,_ : (a : A) → (b : B a) → Σ A B

infixr  _,_

Usage

A dependent pair may represent:

• a disjoint union of a family of (data) types,
• a subset of a set,
• existential quantification.

Σ as disjoint union

Some examples of where Σ could be used as disjoint union:

• List A ~ Σ ℕ (Vec A)
• Σ ℕ Fin is the type that contains all Fins.

Note that the non-dependent pair and the disjoint union of two types are special cases of Σ:

• A × B ~ Σ A (const B)
• A ⊎ B ~ Σ Bool (λ b → if b then A else B)

Σ as subset

If A is a type and P is a predicate on A then we could represent the set of elements that fulfill the predicate by Σ A P.

Examples:

• Vec A n ~ Σ (List A) (λ l → length l ≡ n)
• Fin n ~ Σ ℕ (λ m → m < n)
• balanced trees ~ Σ tree (λ t → t is balanced)

Exercise

Define the toFin function for the Fin′ type.

Fin′ : ℕ → Set
Fin′ n = Σ ℕ (λ x → x < n)

toFin : ∀ {n} → Fin′ n → Fin n

Σ as existential quantification

Let A be a type and let P be a predicate on A. There exists (constructively) an element of A for which P holds iff the subset Σ A P is non-empty.

Examples:

• a ≤ b ~ Σ ℕ (λ k → k + a ≡ b)
• even n ~ Σ ℕ (λ k → n ≡ 2 * k)
• odd n ~ Σ ℕ (λ k → n ≡ 1 + 2 * k)
• a ∈ as ~ Σ ℕ (λ k → as ! k ≡ a)

Note that there we could interpret the Σ A (λ x → P(x)) pattern as ∃ x ∈ A . P(x).

Other use of Σ

Σ can also be very handy when a function needs to return a value together with a proof of that the given value has some property.

For example:

data _∈_ {A : Set}(x : A) : List A → Set where
  first : {xs : List A} → x ∈ x ∷ xs
  next  : {y : A}{xs : List A} → x ∈ xs → x ∈ y ∷ xs

infix  _∈_

_!_ : ∀{A : Set} → List A → ℕ → Maybe A
[]       ! _       = nothing
(x ∷ xs) ! zero    = just x
(x ∷ xs) ! (suc n) = xs ! n

infix  _!_

Exercise

In connection to this example, define the lookup function:

lookup : ∀ {A}{x : A}(xs : List A) → x ∈ xs → Σ ℕ (λ n → xs ! n ≡ just x)

Hint: Use the with keyword.

Exercise

Consider the following definitions that declare the isomorphism (known from earlier) between List ⊤ and ℕ.

fromList : List ⊤ → ℕ
fromList [] = zero
fromList (x ∷ xs) = suc (fromList xs)

toList : ℕ → List ⊤
toList zero = []
toList (suc n) = tt ∷ toList n

lemma : ∀ {a b : ℕ} → Data.Nat.suc a ≡ Data.Nat.suc b → a ≡ b
lemma refl = refl

from-injection : ∀ {a b} → (fromList a) ≡ (fromList b) → a ≡ b
from-injection {[]}      {[]}      refl = refl
from-injection {[]}      {x ∷ xs}  ()
from-injection {x ∷ xs}  {[]}      ()
from-injection {tt ∷ xs} {tt ∷ ys} p = cong (_∷_ tt) (from-injection {xs} {ys} (lemma p))

Now, define the following function:

from-surjection : ∀ (n : ℕ) → Σ (List ⊤) (λ t → (fromList t) ≡ n)

Hint: Use the with keyword.