module Sets.Parameters_vs_Indices where

open import Data.Nat using (ℕ; zero; suc; _≤_; z≤n; s≤s) open import Data.List using (List; []; _∷_)

The *first* index can be turned into a new parameter if each constructor has the same variable on the first index position (that is, in the result type).

*Example 1.*

```
data _≤′_ : ℕ → ℕ → Set where
≤′-refl : {m : ℕ} → m ≤′ m
≤′-step : {m : ℕ} → {n : ℕ} → m ≤′ n → m ≤′ suc n
```

which is similar to

```
data _≤′_ (m : ℕ) : ℕ → Set where
≤′-refl : m ≤′ m
≤′-step : {n : ℕ} → m ≤′ n → m ≤′ suc n
```

*Example 2.*

```
data _≤″_ : ℕ → ℕ → Set where
≤+ : ∀ {m n k} → m + n ≡ k → m ≤″ k
```

which is similar to

```
data _≤″_ (m : ℕ) : ℕ → Set where
≤+ : ∀ {n k} → m + n ≡ k → m ≤″ k
```

which is similar to

```
data _≤″_ (m : ℕ) (k : ℕ) : Set where
≤+ : ∀ {n} → m + n ≡ k → m ≤″ k
```

**Design decision**

It is always a better to use a parameter instead of an index, because:

We suggest more about the structure of the set.* In turn, the Agda compiler can infer more properties of this set.**

Cleaner syntax: each constructor has one parameter less.

*The parameter can be fixed in order to get a simpler definition, c.f.

```
data 10≤′ : ℕ → Set where
10≤′-refl : 10≤′ 10
10≤′-step : {n : ℕ} → 10≤′ n → 10≤′ suc n
```

was made from `_≤′_`

with a simple substitution, which is possible with `_≤_`

.

`_≡_`

Consider the following definition

data _≡_ {A : Set} (x : A) : A → Set where refl : x ≡ x infix 4 _≡_

that yields the following judgements:

```
refl {ℕ} {0} : 0 ≡ 0
refl {ℕ} {1} : 1 ≡ 1
refl {ℕ} {2} : 2 ≡ 2
...
```

so we can come the conclusion that it actually represents equality.

`_∈_`

propositionConsider another parametric definition:

data _∈_ {A : Set}(x : A) : List A → Set where first : ∀ {xs} → x ∈ x ∷ xs next : ∀ {y xs} → x ∈ xs → x ∈ y ∷ xs infix 4 _∈_

Define

`_⊆_ {A : Set} : List A → List A → Set`

.- Prove that
`1 ∷ 2 ∷ [] ⊆ 1 ∷ 2 ∷ 3 ∷ []`

. - Prove that
`1 ∷ 2 ∷ 3 ∷ [] ⊆ 1 ∷ 2 ∷ []`

is false.

- Prove that
Define a predicate for permutations.

Define a predicate for sorting.

Note that you can type `⊆`

as `\sub=`

.