Contents Previous Next

# Sets in Type Theory

```
open import Agda.Primitive using (Level; _⊔_; lsuc; lzero)
open import Types.product
open import Types.relations
open import Types.equality
module Algebra.sets where
```

The concept of set appears in several different guises in mathematics. In type theory, Sets are defiend in a way to “make sense” in a mathematical way. We will revisit the sense part at a later time.

## Setoid

A setoid is a set of objects equipped with an equivalence relation.

```
record Setoid c ℓ : Set (lsuc (c ⊔ ℓ)) where
infix 4 _≃_
field
Data : Set c
_≃_ : Rel Data ℓ
isEquivalence : IsEquivalence _≃_
open IsEquivalence isEquivalence public
```

This concept comes from Bishop who defined the notion of set to be specified by stating that a set has to be given by a description of how to build elements of this set and by giving a binary relation of equality, which has to be an equivalence relation.

Identity Types and Paths