    ------------------------------------------------------------------------
    -- 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