| 12345678910111213141516171819 |
- module Setoids where
- open import Eq
- open import Prelude
- record Setoid : Set1 where
- field
- carrier : Set
- _≈_ : carrier -> carrier -> Set
- equiv : Equiv _≈_
- record Datoid : Set1 where
- field
- setoid : Setoid
- _≟_ : forall x y -> Dec (Setoid._≈_ setoid x y)
- Setoid-≡ : Set -> Setoid
- Setoid-≡ a = record { carrier = a; _≈_ = _≡_; equiv = Equiv-≡ }
|
