------------------------------------------------------------------------
-- Equational resoning for equivalences
------------------------------------------------------------------------

open import Tools.Relation

-- Reasoning for equivalence relations using preorder relation syntax

module Tools.Reasoning.Equivalence {a ℓ} (S : Setoid a ℓ) where

open Setoid S

-- ≈ is a preorder

≈-isPreorder : IsPreorder _≈_ _≈_
≈-isPreorder = record
  { isEquivalence = isEquivalence
  ; reflexive = λ x → x
  ; trans = trans
  }

≈-preorder : Preorder _ _ _
≈-preorder = record
  { Carrier = Carrier
  ; _≈_ = _≈_
  ; _≲_ = _≈_
  ; isPreorder = ≈-isPreorder
  }

open import Tools.Reasoning.Preorder ≈-preorder public