Is this formalization of the empty set correct in Agda?

Question

I'm following The Haskell Road to Logic, Maths and Programming in Agda. The book states:

The empty set is trivially a relation and is the smallest relation between two sets A and B

in Agda:

data ∅ : Set where

record ⊤ : Set where

record Σ (A : Set) (B : A → Set) : Set₁ where
  constructor _,_
  field
    π₁ : A
    π₂ : B π₁

_×_ : Set → Set → Set₁
A × B = Σ A (λ _ → B)
infixr 5 _×_ _,_

Relation : Set → Set₁
Relation P = P × P → Set

With that, I can define relations on specific sets:

lteℕ : Relation ℕ
lteℕ(x , y) = x ≤ℕ y where
  _≤ℕ_ : ℕ → ℕ → Set
  O ≤ℕ O = ⊤
  O ≤ℕ S y = ⊤
  S x ≤ℕ O = ∅
  S x ≤ℕ S y = x ≤ℕ y
  infixr 5 _≤ℕ_

But now I have a problem, because the signature for the empty set relation:

cannot be the empty set, since I already defined it as the unhabited type previously
results in the error Set₁ != Set when checking that the expression Set has type Set even when defined with a distinct symbol as Ø : Relation Set due to the necessity to avoid Russell's paradox in the language.

Is there a way around that that is still logically consistent? Thanks!

@MrO start of chapter 5 (relations). This is not an exercise in particular. I was just going for the basics. — Raoul
what is, in your code, supposed to represent the empty set ? This would help me help you to know that. On a side note and from what I can read in the book, the empty set is said to be trivially a relation simply because a relation is represented by a set of pairs, which, when empty, gives the empty set. — MrO
@MrO the empty set is the first line: data ∅ : Set where which is the unhabited type. I understand the triviality of the definition, but that means that the empty set is a relation between any two sets, isn't it? Therefore, I would expect to be able to say that the empty set has type Ø : Relation Set. No? — Raoul
ok now I understand better what your problem is. I'll try and make an answer as soon as possible. — MrO

MrO MrO · Accepted Answer · 2019-11-15T02:28:05

The answer depends on what you call a set. If by set you mean a representation of the mathematical sets, such as a list, then the empty set is just represented by the empty list.

If by set you mean the Agda Set which means a type, then the answer is a bit more complicated: there is not an empty type, but there are as many as you can think of. More precisely, there are as many empty types as data types for which you don't provide any constructor. The question is then more "which of these types do I chose to model the empty set ?" rather than "how do I model the empty set ?".

Here is an example of an agda module which emphasizes this aspect: First, I have a few imports and the header of my module:

open import Agda.Primitive
open import Data.Nat hiding (_⊔_)

module EmptySets where

Then I start by an empty type, the more simple you can think of:

data Empty : Set where

From this data type, it is possible to write an eliminator:

Empty-elim : ∀ {a} {A : Set a} → Empty → A
Empty-elim ()

This basically says that anything holds if Empty holds.

But, I could have also chosen to represent the empty set as the empty relation by defining a family of types, all empty, which are all relations. First, relations needs to be defined (I took the definition from the standard library):

REL : ∀ {a b} → Set a → Set b → (ℓ : Level) → Set (a ⊔ b ⊔ lsuc ℓ)
REL A B ℓ = A → B → Set ℓ

Then the family of empty relations can be defined :

data EmptyRelation {a b ℓ} {A : Set a} {B : Set b} : REL A B ℓ where

Since all these types are empty, they all provide an eliminator as well:

EmptyRelation-elim : ∀ {a b x ℓ} {A : Set a} {B : Set b} {X : Set x} {u : A} {v : B} → EmptyRelation {ℓ = ℓ} u v → X
EmptyRelation-elim ()

And, as a consequence, it is possible to instantiate this generic type to get a specific empty type, for instance, the empty relation over natural numbers, which never holds:

EmptyNaturalRelation : REL ℕ ℕ lzero
EmptyNaturalRelation = EmptyRelation

This is what is explained in the book: since a relation is a set of pairs, then the empty type is the smallest of this relation: the one where there are no pairs in it.

But you could also use predicates instead of relations, saying that the empty set is the smallest predicate over a given type: the one that never holds, in which case this is represented as the following:

Pred : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ lsuc ℓ)
Pred A ℓ = A → Set ℓ

data EmptyPredicate {a ℓ} {A : Set a} : Pred A ℓ where

And you could be even crazier and decide to model the empty set as the following:

data EmptySomething {a} {A B C D E Z : Set a} : A → B → C → D → E → Z → Set where

All in all, there are no empty set in agda, but there are a potential infinity of empty types.

As for the code you presented in your question, there are several inaccuracies:

The relations are usually defined on two arguments instead of pairs of argument, which you can then curry on if needed to make them take a pair as parameter.
Why would you make lteℕ depend on _≤ℕ_ and not define it directly ?
You should define lteℕ as a data type rather than a function which returns either bottom or top, which will allow you to case-split on such a term in the future. Usually, this is defined this way (in the standard library):
```
data _≤_ : Rel ℕ 0ℓ where
z≤n : ∀ {n}                 → zero  ≤ n
s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
```

Is this formalization of the empty set correct in Agda?

1 Answers