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

module IsEquivalenceInstances where
    module ForProd {a} {A B : Set a}
        (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
        (eA : IsEquivalence A _≈₁_) (eB : IsEquivalence B _≈₂_) where

        infix 4 _≈_

        _≈_ : A × B → A × B → Set a
        (a₁ , b₁) ≈ (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂)

        ProdEquivalence : IsEquivalence (A × B) _≈_
        ProdEquivalence = record
            { ≈-refl = λ {p} →
                ( IsEquivalence.≈-refl eA
                , IsEquivalence.≈-refl eB
                )
            ; ≈-sym = λ {p₁} {p₂} (a₁≈a₂ , b₁≈b₂) →
                ( IsEquivalence.≈-sym eA a₁≈a₂
                , IsEquivalence.≈-sym eB b₁≈b₂
                )
            ; ≈-trans = λ {p₁} {p₂} {p₃} (a₁≈a₂ , b₁≈b₂) (a₂≈a₃ , b₂≈b₃) →
                ( IsEquivalence.≈-trans eA a₁≈a₂ a₂≈a₃
                , IsEquivalence.≈-trans eB b₁≈b₂ b₂≈b₃
                )
            }