After the Agda Records Tutorial

```
module Sets.Records where

open import Data.Nat
open import Data.Bool
open import Relation.Binary.PropositionalEquality using (_≡_)
import Relation.Binary.PropositionalEquality as Eq```

# Record set definitions

A record type is a special set for representing tuples of values. For example, the following set represents a `Bool`, `ℕ` pair:

```
record R : Set where
field
r₁ : Bool
r₂ : ℕ```

# Record value definitions

An example:

```
x : R
x = record { r₁ = true; r₂ = 2 }```

# Record value definitions with constructors

One could define a constructor for `R` values:

```
r : Bool → ℕ → R
r b n = record { r₁ = b; r₂ = n }

x′ = r true 2```

Agda provides this definition to us with the following syntax:

```
record R′ : Set where
constructor r′   -- record constructor
field
r₁ : Bool
r₂ : ℕ

x″ = r′ true 2```

# Field selectors

Agda defines field selectors automatically:

```
sel₁ : R → Bool
sel₁ = R.r₁

sel₂ : R → ℕ
sel₂ = R.r₂

x‴ = r (R.r₁ x) (R.r₂ x)```

# `record` vs. `data` definitions

For every set defined with `record` there is an equivalent set defined with `data`.

For example, the following set is equivalent to `R`:

```
data R″ : Set where
r″ : (r₁ : Bool) (r₂ : ℕ) → R″

r₁ : R″ → Bool
r₁ (r″ a b) = a

r₂ : R″ → ℕ
r₂ (r″ a b) = b```

Records have the following advantages over `data` definitions:

• A record is definitionally equivalent to its recombined parts:

```
extRec : (x : R) → x ≡ r (R.r₁ x) (R.r₂ x)
extRec _ = Eq.refl

-- {- not possible -}
-- extData : (x : R″) → x ≡ r″ (r₁ x) (r₂ x)
-- extData _ = refl```

It is advised to use `record` definitions whenever it is possible.

# Exercises

• Define `⊤` as a record!
• Define `_×_` as a record!

# Dependent records

The type of a field can depend on the values of the previous fields.

For example the following set is equivalent to `List ℕ`:

```
open import Data.Vec using (Vec; []; _∷_)

record Listℕ : Set where
constructor Lℕ
field
length : ℕ
vector : Vec ℕ length

list : Listℕ
list = Lℕ 3 (0 ∷ 1 ∷ 2 ∷ [])

list′ : Listℕ
list′ = Lℕ _ (0 ∷ 1 ∷ 2 ∷ [])```

The type of the selector functions:

```
length′ : Listℕ → ℕ
length′ = Listℕ.length

vector′ : (x : Listℕ) → Vec ℕ (length′ x)   -- dependent
vector′ = Listℕ.vector```

# Parameterised record

The previous example parameterised with the types of the vector elements:

```
record List (A : Set) : Set where
constructor L
field
length : ℕ
vector : Vec A length

list₂ : List Bool
list₂ = L _ (true ∷ false ∷ true ∷ [])```

The type of the selector functions:

```
length″ : {A : Set} → List A → ℕ
length″ = List.length

vector″ : {A : Set} (x : List A) → Vec A (length″ x)   -- dependent
vector″ = List.vector```

Note that the parameters became implicit in the field selectors' type.
(This is a design decision of the Agda language.)

# Exercises

Define `Σ` with `record`!

TODO

# Exercise

Define the predicate of being an equivalence relation!

```
record IsEquivalence {A : Set} (_≈_ : A → A → Set) : Set where```

Prove that `_≡_` is an equivalence relation on any set!

```
isEquivalence : {A : Set} → IsEquivalence {A} _≡_```

# Exercise

Define the predicate of being a semigroup!

Prove that `ℕ` is a semigroup with `_+_`!