module Sets.Sigma where

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 (⊥)

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 4 _,_

A dependent pair may represent:

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

`Σ`

as disjoint unionSome examples of where `Σ`

could be used as disjoint union:

`List A`

~`Σ ℕ (Vec A)`

`Σ ℕ Fin`

is the type that contains all`Fin`

s.

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 subsetIf `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`)`

Define the `toFin`

function for the `Fin′`

type.

Fin′ : ℕ → Set Fin′ n = Σ ℕ (λ x → x < n) toFin : ∀ {n} → Fin′ n → Fin n

`Σ`

as existential quantificationLet `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)`

.

`Σ`

`Σ`

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 4 _∈_ _!_ : ∀{A : Set} → List A → ℕ → Maybe A [] ! _ = nothing (x ∷ xs) ! zero = just x (x ∷ xs) ! (suc n) = xs ! n infix 5 _!_

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.

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.