Setoid is a record type in Agda, and it appears everywhere from `Relation.Binary.EqReasoning`

to `Algebra`

. But, why do we need such a type ? After reading “setoids in type theory”, I thought that setoids are used for mathematical constructions like subset, quotients in the intensional type theory and the Calculus of Inductive Construction. Since some of functional data structure could be represented as such constructions, it also may be useful for functional programming, at least for understanding it.

Setoid is defined as a record type as follows,

`record Setoid : Set1 where`

infix 4 _≈_

field

`carrier : Set`

_≈_ : Rel carrier

isEquivalence : IsEquivalence _≈_

where `isEquivalence`

is a record type packing the proof of equivalence relation defined as follows,

`record IsEquivalence {a : Set} (_≈_ : Rel a) : Set where`

field

`refl : Reflexive _≈_`

sym : Symmetric _≈_

trans : Transitive _≈_

Usually, we call such a setoid is a “total” setoid since it’s defined on all elements of type “`carrier`

“. We will explan what is the meaning of each field.

`carrier : Set`

: the underlaying type what we want to operate on,`_≈_ : Rel`

: the relation what we think the equality between elements of “carrier”,`isEquivalence : IsEquivalence _≈_`

: the proof terms which show that _≈_ is a equivalence relation.

Thus, there is a induced setoid from Leibniz equality (see `Relation.Binary.Core`

) for evey types, that is, we have a setoid for every type A, by computationally equality (“for all x in A, x ≡ x”). You could find such induced setoid from `Relation.Binary.PropositionalEquality.≡-setoid`

defined on all types.

However, we could define other equivalence relation. For example, we want to identify lists with the same length, and we could define it as follows,

`data _∼_ {a : Set}(xs : List a) : (List a) → Set where`

`len-eq : {ys : List a} → (pf : length xs ≡ length ys) → xs ∼ ys`

It’s obvious to see that it’s a equivalence relation, and we could give proof terms about it.

`∼-refl : ∀ {a} → {xs : List a} → xs ∼ xs`

∼-refl = len-eq ≡-refl

`∼-sym : ∀ {a} → {xs ys : List a} → xs ∼ ys → ys ∼ xs`

∼-sym (len-eq refl) = len-eq (≡-sym refl)

`∼-trans : ∀ {a} → {xs ys zs : List a} → xs ∼ ys → ys ∼ zs → xs ∼ zs`

∼-trans (len-eq xs∼ys) (len-eq ys∼zs) = len-eq (≡-trans xs∼ys ys∼zs)

It’s trivial since they use the fact from Leibnz equality. Finally, we could pack them together simply by define it as a `Setoid`

by hand, but we notice that it is just as same as defining a quotient on `≡-setoid (List a)`

. Hence, we define a function `Quotient`

to do this,

`Quotient : (S : Set)(_∼_ : Rel S)(ER : IsEquivalence _∼_) → Setoid`

Quotient S _∼_ ER = record

`{ carrier = S`

; _≈_ = _∼_

; isEquivalence = ER

}

Thus, the following is .

`ListLen : (a : Set) → Setoid`

ListLen a = Quotient (List a) _∼_ ∼-isEQ

`where`

`∼-isEQ : IsEquivalence (_∼_ {a})`

∼-isEQ = record

`{ refl = ∼-refl`

; sym = ∼-sym

; trans = ∼-trans

}

We could show that `ListLen`

is equivalent to by constructing a function from `ListLen`

to and its inverse. Notice that, it’s exactly the function `Data.List.length`

and `Data.List.replicate`

. From these function, we could define “plus” from “concatenate” by such mapping from `ListLen`

to . It means that we could define an operation on a more delicated structure, and get the operation on its quotient, via .

Thanks for the explanation! I didn’t quite understand what Setoid was for.

Questions:

> We could show that ListLen is equivalent to N by constructing a function from ListLen to and its inverse.

You mean from the carrier of ListLen to N, right?

> It means that we could define an operation on a more delicated structure, and get the operation on its quotient, via…

It’d be great to know how to do that!

No, I mean a map from a setoid to a setoid. So I must give it a proof that the

`length`

and`replicate`

preserve the equality.It may look a bit strange such that I define _∼_ by Nat. However, we could avoid it as follows,

`data _∼_ {a : Set} : (List a) → (List a) → Set where`

[]-eq : [] ∼ []

∷-eq : ∀ {xs ys x y} → (xs∼ys : xs ∼ ys) → (x ∷ xs) ∼ (y ∷ ys)

The proof of this equivalence relation is also easy with pattern matching. Thus we could define

`plus'`

on Nat (Setoid) by composition with`++`

and`length`

. Then, define the extracted function`(Map.ap plus')`

as`plus`

. Hummm, I haven’t yet written about`Map`

, and I think I will post it later.Pingback: Decidable setoid in Agda « XOO’s

A few years have passed since this post. I am not able to find \==-refl and \==-setoid in the current agda libraries. Could you please provide a current pointer ?

Hi, I am not so sure about your question. You may start from Relation.Binary for a definition of equivalence relation.