------------------------------------------------------------------------
-- The Agda standard library
--
-- Substituting equalities for binary relations
------------------------------------------------------------------------

-- For more general transformations between binary relations
-- see `Relation.Binary.Morphisms`.

{-# OPTIONS --cubical-compatible --safe #-}

open import Data.Product.Base as Prod
open import Relation.Binary.Core using (Rel; _⇔_)
open import Relation.Binary.Structures using (IsEquivalence)
open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive)

module Relation.Binary.Construct.Subst.Equality
  {a ℓ₁ ℓ₂} {A : Set a} {≈₁ : Rel A ℓ₁} {≈₂ : Rel A ℓ₂}
  (equiv@(to , from) : ≈₁ ⇔ ≈₂)
  where

open import Function.Base

------------------------------------------------------------------------
-- Definitions

refl : Reflexive ≈₁ → Reflexive ≈₂
refl refl = to refl

sym : Symmetric ≈₁ → Symmetric ≈₂
sym sym = to ∘′ sym ∘′ from

trans : Transitive ≈₁ → Transitive ≈₂
trans trans x≈y y≈z = to (trans (from x≈y) (from y≈z))

------------------------------------------------------------------------
-- Structures

isEquivalence : IsEquivalence ≈₁ → IsEquivalence ≈₂
isEquivalence E = record
  { refl  = refl  E.refl
  ; sym   = sym   E.sym
  ; trans = trans E.trans
  } where module E = IsEquivalence E