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 Function 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

The dependent pair may represent

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

Σ as disjoint union

Examples:

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

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 can represent the set of elements which fulfil 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 toFin:

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 nonempty.

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)

Exercise

Sigma is very handy when a function needs to return a value and a proof that the value has some property.

Example:

data _∈_ {A : Set}(x : A) : List A → Set where
  first : {xs : List A} → x ∈ x ∷ xs
  later : {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  _!_

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

Define lookup!

Exercise

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

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

lemm : ∀ {a b : ℕ} → Data.Nat.suc a ≡ Data.Nat.suc b → a ≡ b
lemm 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} (lemm p)

Define the following function:

from-surjection : ∀ (n : ℕ) → Σ (List ⊤) (_≡_ n ∘ fromList)