# Unary Relation Examples

Lately I’ve been learning the dependently typed programming language
Agda.
While it’s a joy to learn, learning materials for the Agda standard library are
sparse. In this post, I give examples using of the `stdlib`

’s
`Relation.Unary`

module to do elementary set
theory. The logical propositions I prove herein are rather trivial,
but for newbies to dependently-typed
languages like me, even the trivial can seem hard.

## Preliminaries

You can read this post without knowing any Agda. If nothing else, you can get a hint of the kinds of things you can do with the concept and an implementation of propositions as types.

I make reference to the Programming Language Foundations in Agda (PLFA) online book, and I highly recommend (at least chapter 1) for learning the basics of Agda.

### Basic Structure

The examples follow this structure:

```
_ : Proposition
_ = Proof
```

To the right of the `:`

is a claim, a proposition. To the
right of the `=`

is a proof of that claim. The `_`

on both lines just means I haven’t given this expression a name.

## Predicates

Prior to learning Agda/type theory/etc, I understood the term
predicate to mean a unary function (function of one argument) that
returns a boolean (i.e. true or false): `A → Bool`

. This view
of predicates as indicator functions turns out to be rather limited
understanding. Another, richer, understanding sees predicates as unary
functions to `Set`

(the collection of all types):
`A → Set`

. Here’s a hint
at what this is all about. and here’s a description from the `Relation.Unary`

docs:

```
-- Unary relations are known as predicates and `Pred A ℓ` can be viewed
-- as some property that elements of type A might satisfy.
-- Consequently `P : Pred A ℓ` can also be seen as a subset of A
-- containing all the elements of A that satisfy property P. This view
-- informs much of the notation used below.
```

## Setup

## Show module setup and imports.

First, create a module. The name of the top-level module of in a file should match the filename.

`module index where`

By `import`

ing `Relation.Unary`

module, we get
access to its contents. The `open`

statement brings the
module’s content into scope as if the names were define within the
current module. Without the `open`

statement, we’d have to
qualify all the names to use them, as in
`Relation.Unary._∈_`

.

`open import Relation.Unary`

Other imports we’ll need:

```
open import Data.Unit using ( tt )
open import Level
open import Relation.Binary.PropositionalEquality using ( refl )
open import Relation.Nullary using ( ¬_ )
open import Relation.Nullary.Negation using ( contradiction )
open import Data.Product
open import Data.Sum.Base using (_⊎_; inj₁ ; inj₂ ; [_,_]′ )
```

## Example Set

Here’s the three element set I’ll work with in the examples:

\[ \{ Orange, Apple, Banana \} \]

This set can be defined in adga as a simple datatype:

```
data Fruit : Set where
: Fruit Orange Apple Banana
```

## Example Propositions/Proofs

In each of the examples below, I show how to one can prove the proposition in the header. So for example, the first proposition is that \(Orange \in \{ Orange \}\), i.e. \(Orange\) is in the singleton set containing \(Orange\). This should hopefully be easy to prove.

### Set inclusion

#### \(Orange \in \{ Orange \}\)

Indeed, to prove the proposition, we state `refl`

, which
stands for reflexity.

```
_ : Orange ∈ ｛ Orange ｝
_ = refl
```

Inlining ∈ and ｛_｝ step by step might make it easier to see what’s going on:

```
Orange ∈ ｛ Orange ｝
== ｛ Orange ｝ Orange ( x ∈ P = P x )
== Orange = Orange ( ｛ x ｝ = x ≡_)
```

Proof of the statement `Orange = Orange`

is
`refl`

.

#### \(\neg ( Banana \in \{ Orange \} )\)

The claim \(Banana \in \{ Orange \}\) should not hold; i.e., we should be able to construct a proof of the negation of the claim.

```
_ : ¬ ( Banana ∈ ｛ Orange ｝ )
_ = λ()
```

In this case, we can use an absurd pattern:

Absurd patterns can be used when none of the constructors for a particular argument would be valid.

This is indeed the case here, as we cannot construct a proof that
`Banana = Orange`

. For more on negation in constructive logic
and Agda, see the negation
chapter in PLFA.

I’ll note that the proposition above is equivalent to the following
by definition of `_∉_`

:

```
_ : Banana ∉ ｛ Orange ｝
_ = λ()
```

#### \(Orange \in \{ Orange, Apple \}\)

Now I move beyond singleton sets and define a subset containing both
\(Orange\) and \(Apple\). This is straighforward with the
union `_∪_`

operator:

```
: Pred Fruit _
O∪A = ｛ Orange ｝ ∪ ｛ Apple ｝ O∪A
```

The union operator constructs a Sum
type, which I think of as the proposition that either the
`｛ Orange ｝`

claim or the `｛ Apple ｝`

claim
holds. Hence to prove the claim, we give a proof of \(Orange \in \{ Orange \}\) to the first
(`inj₁`

) position in the sum.

```
_ : Orange ∈ O∪A
_ = inj₁ refl
```

For more on the sum type, see the Disjunction as Sum section in PLFA.

#### \(Orange \in \{ Orange, Apple, Banana \}\)

The `U`

symbol represents the univeral set for a type. I find that symbol
hard to distinguish from the union operator and infinitary union, so
I’ll give the set \(\{ Orange, Apple, Banana
\}\) a name.

```
: Pred Fruit _
allFruit = U allFruit
```

The examples holds trivially because `allFruit`

is the
universal set of `Fruit`

.

```
_ : Orange ∈ allFruit
_ = tt
```

I’ll inline the proposition again to see what is needed of the proof.

```
Orange ∈ allFruit
== allFruit Orange ( by definition )
== U Orange ( by definition )
== (λ _ → ⊤) Orange ( by definition )
== ⊤ ( function application )
```

So we need a term of type `⊤`

, for which `tt`

is the only constructor for the `⊤`

(unit) type.

### Subset relations

I’ll switch from proofs about set inclusion to proofs on subset relations.

The subset relation states that a proof `P`

is a subset of
`Q`

is evidence that for all x in `P`

, x is also
in `Q`

. Or in agda:

```
_⊆_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
P ⊆ Q = ∀ {x} → x ∈ P → x ∈ Q
```

#### \(\{ Orange, Apple \} \subseteq \{ Orange, Apple, Banana \}\)

The first one is simple:

```
_ : O∪A ⊆ allFruit
_ = λ _ → tt
```

#### \(\{ Orange \} \cap \{ Orange, Apple \} \subseteq \{ Orange \}\)

```
_ : ( ｛ Orange ｝ ∩ O∪A ) ⊆ ｛ Orange ｝
_ = λ ｛O｝∩O∪A → proj₁ ｛O｝∩O∪A
```

Again inlining the claim might it more clear why the evidence I provided is proof of the claim.

```
∀ {x} → x ∈ ( ｛ Orange ｝ ∩ O∪A ) → x ∈ ｛ Orange ｝ (definition of _⊆_)
== ∀ {x} → (λ y → y ∈ ｛ Orange ｝ × y ∈ O∪A ) x → x ∈ ｛ Orange ｝ (definition of _∩_)
== ∀ {x} → x ∈ ｛ Orange ｝ × x ∈ O∪A → x ∈ ｛ Orange ｝ (function application )
```

Ignoring the `∀ {x}`

, the claim states that proof is a
function that take the product of `x ∈ ｛ Orange ｝`

and
`x ∈ O∪A`

and returns `x ∈ ｛ Orange ｝`

, which is
exactly what I wrote. Note that I could just as well have written:
`λ x → proj₁ x`

. The name of lambda variable is irrelevant,
but I used the name `｛O｝∩O∪A`

to give a visual cue what
type is being passed.

#### \(\{ Banana \} \not\subseteq \{ Orange, Apple \}\)

This one is little trickier:

```
_ : ｛ Banana ｝ ⊈ O∪A
_ = λ b⊆O∪A → [ ( λ () ) , ( λ () ) ]′ (b⊆O∪A refl)
```

I used the `[_,_]′`

function. to produce a term of
`¬ (｛ Banana ｝ ⊆ O∪A )`

.

### Equality of `Pred`

Now that we have an idea how to prove subset relations; I’ll
demonstrate proofs for equality of predicates. Predicate equality is
defined in recent versions of `Relation.Unary`

, but for some
reason, it’s not in the version I’m using, so I define it here:

```
_≐_ : ∀ { ℓ₁ ℓ₂ : Level } { C : Set } → Pred C ℓ₁ → Pred C ℓ₂ → Set _
= (P ⊆ Q) × (Q ⊆ P) P ≐ Q
```

I won’t go through these in detail. I will reiterate that proof in
each case involves producing a pair proofs, one for `P ⊆ Q`

and another for `Q ⊆ P`

.

#### \(\{ Orange \} \cap \{ Orange, Apple, Banana \} = \{ Orange \}\)

```
_ : ( ｛ Orange ｝ ∩ allFruit ) ≐ ( ｛ Orange ｝ )
_ = (λ ( o∈O , _ ) → o∈O )
( λ o∈O → o∈O , tt ) ,
```

#### \(\{ Orange \} \cap \{ Apple \} = \emptyset\)

```
_ : ( ｛ Orange ｝ ∩ ｛ Apple ｝ ) ≐ ∅
_ = ( λ { (refl , ())})
( λ () ) ,
```

#### \(\{ Orange \} \cup \{ Apple \} \cup \{ Banana \} = \bigcup\)

```
_ : ( ｛ Orange ｝ ∪ ｛ Apple ｝ ∪ ｛ Banana ｝ ) ≐ allFruit
_ = ( λ _ → tt )
λ { {Orange} _ → inj₁ refl
, ; {Apple} _ → inj₂ (inj₁ refl)
; {Banana} _ → inj₂ (inj₂ refl)
}
```

## Fin

I hope to share more of my Agda learnings in the coming weeks.