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

Usage

A dependent pair may represent:

Σ as disjoint union

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

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

Σ 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:

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:

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

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

infix 5 _!_

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.