------------------------------------------------------------------------
-- The Agda standard library
--
-- Function setoids and related constructions
------------------------------------------------------------------------

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

module Function.Indexed.Relation.Binary.Equality where

open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Indexed.Heterogeneous using (IndexedSetoid)

-- A variant of setoid which uses the propositional equality setoid
-- for the domain, and a more convenient definition of _≈_.

≡-setoid :  {f t₁ t₂} (From : Set f)  IndexedSetoid From t₁ t₂  Setoid _ _
≡-setoid From To = record
  { Carrier       = (x : From)  Carrier x
  ; _≈_           = λ f g   x  f x  g x
  ; isEquivalence = record
    { refl  = λ {f} x  refl
    ; sym   = λ f∼g x  sym (f∼g x)
    ; trans = λ f∼g g∼h x  trans (f∼g x) (g∼h x)
    }
  } where open IndexedSetoid To