Basic Set Theory

The source code for this module: PartII/Sets.ard
The source code for the exercises: PartII/SetsEx.ard

The types, which are sets according to the view adopted in the last modules, behave like sets in set theory. This means that many theorems of set theory can be proven for the sets in this sense.

For example, we can prove the Cantor’s theorem saying that the cardinality of a set X is strictly less than the cardinality of the set of its subsets X -> \Prop.

The assertion that the cardinality is less (not necessarily strictly) means that there exists injection of X into X -> \Prop. Clearly, the equality predicate (=) : X -> (X -> \Prop) is an injection.

The assertion that the cardinality is strictly less means that, in addition, there is no surjection f : X -> (X -> \Prop). This can be easily proven by adopting the classical Cantor’s argument.

Note, however, that a number of theorems of the classical set theory are not provable in type theory without assuming the excluded middle or the axiom of choice. For example, the Schroder-Bernstein theorem, which says that if for two sets there exist injective functions both ways between them then there exists a bijection between them, is not provable without excluded middle.

Surjections, injections and bijections

We have already seen the definitions of injection and surjections, but let us briefly recall it. Note that the definition of surjection requires the propositional truncation.

\func isInj {A B : \Set} (f : A -> B) => \Pi (x y : A) -> f x = f y -> x = y

\truncated \data Trunc (A : \Type) : \Prop
  | in A
  \where {
    \func map {A B : \Type} (f : A -> B) (x : Trunc A) : Trunc B \elim x
      | in a => in (f a)

    \lemma extract {A : \Type} (x : Trunc A) (p : isProp A) : \level A p \elim x
      | in a => a
  }

-- Note that \Sigma (a : A) (f a = b) is not
-- necessarily a proposition and should be truncated.
\func isSur {A B : \Set} (f : A -> B) : \Prop =>
     \Pi (b : B) -> Trunc (\Sigma (a : A) (f a = b))
  -- \Pi (b : B) ->        \Sigma (a : A) (f a = b)

We now give an obvious definition of a bijection and prove that bijectivity is a conjunction of injectivity and surjectivity.

\func isBij {A B : \Set} (f : A -> B) => \Sigma (g : B -> A) (\Pi (x : A) -> g (f x) = x) (\Pi (y : B) -> f (g y) = y)

\func isBij->isInj {A B : \Set} (f : A -> B) (p : isBij f) : isInj f => \lam x y q => sym (p.2 x) *> pmap p.1 q *> p.2 y

\func isBij->isSur {A B : \Set} (f : A -> B) (p : isBij f) : isSur f => \lam b => in (p.1 b, p.3 b)

\func sigmaEq' {A : \Type} (B : A -> \Prop) (t1 t2 : \Sigma (x : A) (B x)) (p : t1.1 = t2.1)
  => sigmaEq B t1 t2 p (Path.inProp _ _)

\func isInj+isSur->isBij {A B : \Set} (f : A -> B) (ip : isInj f) (sp : isSur f) : isBij f
  => \let t (b : B) => Trunc.extract (sp b) (\lam t1 t2 => sigmaEq' (\lam a => f a = b) t1 t2 (ip t1.1 t2.1 (t1.2 *> sym t2.2)))
     \in (\lam b => (t b).1, \lam a => ip _ _ (t (f a)).2, \lam b => (t b).2)

Exercise 1: Prove that the predecessor function pred on Nat is surjective.

Exercise 2: Prove that suc is not surjective.

Exercise 3: Let f : A -> B and g : B -> C be some functions. Prove that if f and g are surjective, then g o f is also surjective. Prove that if g o f is surjective, then g is also surjective.

Exercise 4: Prove the Cantor’s theorem.

A definition of Int, datatypes with conditions

Here we introduce a useful construct for data definitions, which allows quotioning or, in other words, gluing, and apply it to the definition of the type Int of integers.

Consider first the definition of the type of integers as the ordinary datatype containing two copies of Nat: nonnegative and nonpositive numbers.

\data Int'
  | pos' Nat
  | neg' Nat

Totalities of elements defined by different constructors in an ordinary datatype do not intersect. For example, we can prove that pos’ n is always not equal to neg’ m. Sometimes it is not convenient: for example, we would like pos’ 0 to be the same as neg’ 0.

It is possible to specify such identifications of constructors by supplementing definitions of constructors with conditions. The syntax for conditions is the same as for functions defined by pattern matching. The only differences are that some cases can be uncovered and matching on the interval type I is allowed.

Let us modify the definition of integers as follows:

\data Int
  | pos Nat
  | neg (n : Nat) \elim n {
    | 0 => pos 0
  }

The new definition Int now has a useful property that neg 0 evaluates to pos 0.

Whenever a function over such a type is defined, the typechecker checks if its values on equivalent constructors coincide. For example, the following definition does not typecheck, because intEx (pos 0) is 3, but intEx (neg 0) is 7:

-- This does not typecheck!
\func intEx (z : Int) : Nat
  | pos n => 3
  | neg n => 7

We can fix this by replacing the second pattern with neg (suc n) and omitting the pattern neg 0 since it evaluates:

\func intEx' (z : Int) : Nat
  | pos n => 3
  | neg (suc n) => 7

Let us give a couple of examples of functions over Int:

\func negative (x : Int) : Int
  | pos n => neg n
  | neg n => pos n

\func abs (x : Int) : Nat
  | pos n => n
  | neg n => n

Exercise 5: Define the function negPred : Int -> Int such that negPred x = x if x > 0 and negPred x = x - 1 if x <= 0.

Exercise 6: Define addition and multiplication for Int.

Exercise 7: Define the datatype BinNat for the binary natural numbers. It should have three constructors: for 0, for even numbers 2n and for odd numbers 2n+1. This type contains several different representations of zero. Use datatypes with conditions to identify different representations of zero.

Exercise 8: Define mutually inverse functions Nat -> BinNat and BinNat -> Nat and prove that they are mutually inverse.

Quotient sets

Let A be a set together with an equivalence relation ~ on it. We can define the quotient set A/~ together with the function in~ : A -> A/~ such that any two equivalent elements of A are identified in A/~.

A : \Set
~ : A -> A -> \Prop
A/~ : \Set
in~ : A -> A/~
(in~ a = in~ a') <-> (a ~ a')

A function over A/~ can be defined as a function over A satisfying the condition that equivalent elements are mapped to equal elements. With the proof of the condition omitted and using simplified syntax (the full definition is given below) we can write:

-- A simplification. This is not intended to be typechecking.
\func f (x : A/~) : B
   | in~ a => b

An important of example of quotient set – the set of rational numbers, which is defined as the set of pairs of natural numbers quotioned by the equivalence relation ~ such that (n, m) ~ (n’, m’) iff n * m’ = n’ * m.

We can define the quotient set as a datatype with conditions: we simply add an equality between inR a and inR a’ if R a a’.

\truncated \data Quotient (A : \Type) (R : A -> A -> \Type) : \Set
  | inR A
  | eq (a a' : A) (r : R a a') (i : I) \elim i {
    | left => inR a
    | right => inR a'
  }

Note that we have to use the truncation to the level of sets, otherwise we will not get a set.

The equivalent elements are indeed equal:

\func quotientEq {A : \Type} {R : A -> A -> \Type} (a a' : A) (r : R a a')
  : inR a = {Quotient A R} inR a'
  => path (eq a a' r)

We can prove, for example, that inR is surjective:

\func inR-sur {A : \Type} {R : A -> A -> \Type} : isSur (inR {A} {R}) =>
  \lam [a] => \case \elim [a] \with {
    | inR a => in (a, idp)
  }

If we want to define a function over Quotient A R we need to define a function on elements of the form inR a and on the constructor eq. The latter corresponds to a proof that the function maps equivalent elements to equal values.

\func quotientEx {A : \Type} {R : A -> A -> \Type} {B : \Set}
                 (f : A -> B) (p : \Pi (a a' : A) -> R a a' -> f a = f a')
                 (x : Quotient A R) : B \elim x
  | inR a => f a
  | eq a a' r i => p a a' r @ i

Exercise 9: Define the set of finite subsets of a set A, that is of finite lists of elements of A defined up to permutations and repetitions of elements.