{-# OPTIONS --cubical-compatible --safe #-}
open import Level using (Level; _⊔_)
open import Relation.Binary.Bundles using (Setoid)
module Function.Relation.Binary.Setoid.Equality {a₁ a₂ b₁ b₂ : Level}
(From : Setoid a₁ a₂) (To : Setoid b₁ b₂) where
open import Function.Bundles using (Func; _⟨$⟩_)
open import Relation.Binary.Definitions
using (Reflexive; Symmetric; Transitive)
open import Relation.Binary.Structures
using (IsEquivalence)
private
module To = Setoid To
module From = Setoid From
infix 4 _≈_
_≈_ : (f g : Func From To) → Set (a₁ ⊔ b₂)
f ≈ g = {x : From.Carrier} → f ⟨$⟩ x To.≈ g ⟨$⟩ x
refl : Reflexive _≈_
refl = To.refl
sym : Symmetric _≈_
sym = λ f≈g → To.sym f≈g
trans : Transitive _≈_
trans = λ f≈g g≈h → To.trans f≈g g≈h
isEquivalence : IsEquivalence _≈_
isEquivalence = record
{ refl = λ {f} → refl {f}
; sym = λ {f} {g} → sym {f} {g}
; trans = λ {f} {g} {h} → trans {f} {g} {h}
}
setoid : Setoid _ _
setoid = record { isEquivalence = isEquivalence }
infixr 9 _⇨_
_⇨_ : Setoid _ _
_⇨_ = setoid