Contents Previous Next

• Sets in Type Theory
  • Setoid

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