module Equivalence where

open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
open import Relation.Binary.Definitions
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym)

module _ {a} (A : Set a) (_≈_ : A → A → Set a) where
    IsReflexive : Set a
    IsReflexive = ∀ {a : A} → a ≈ a

    IsSymmetric : Set a
    IsSymmetric = ∀ {a b : A} → a ≈ b → b ≈ a

    IsTransitive : Set a
    IsTransitive = ∀ {a b c : A} → a ≈ b → b ≈ c → a ≈ c

    record IsEquivalence : Set a where
        field
            ≈-refl : IsReflexive
            ≈-sym : IsSymmetric
            ≈-trans : IsTransitive