# PLFA: Relations

Mar 3 2023 · LastMod: Mar 3 2023

Programming Language Foundations in Agda, Relations: Inductive definition of relations.

Dependent types are introduced in a very confusing way. Here is some explanation. The definition of `≤`

is given by

```
1data _≤_ : ℕ → ℕ → Set where
2 z≤n : ∀ {n : ℕ} → zero ≤ n
3 s≤s : ∀ {m n : ℕ} → m ≤ n → suc m ≤ suc n
4s
```

Note the implicit argument marked by the apperance of curly brackets `{}`

. Here `zero ≤ n`

, `m ≤ n`

, `suc m ≤ suc n`

are all *dependent types*, or family of types (remember Curry-Howard). `z≤n`

and `s≤s`

are *type constructors*. For fixed `n:ℕ`

, `zero ≤ n`

is *a* type.

The proof of `_ : 2 ≤ 4`

, given by

```
1_ : 2 ≤ 4
2_ = s≤s (s≤s z≤n)
```

is really

```
1_ = s≤s {1} {3} (s≤s {0} {2} (z≤n {2}))
```

where

- the type
`z≤n {2}`

is`zero ≤ 2`

, - the type
`s≤s {0} {2}`

is`suc 0 ≤ suc 2`

, - the type
`s≤s {1} {3}`

is`suc 2 ≤ suc 4`

.