12 lines
455 B
Agda
12 lines
455 B
Agda
module Equivalence where
|
||
|
||
open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
|
||
open import Relation.Binary.Definitions
|
||
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym)
|
||
|
||
record IsEquivalence {a} (A : Set a) (_≈_ : A → A → Set a) : Set a where
|
||
field
|
||
≈-refl : {a : A} → a ≈ a
|
||
≈-sym : {a b : A} → a ≈ b → b ≈ a
|
||
≈-trans : {a b c : A} → a ≈ b → b ≈ c → a ≈ c
|