diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
index 42430b90ea..d053f3f3b5 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
@@ -23,7 +23,6 @@ open import Data.List.Membership.Propositional.Properties
 import Data.List.Properties as Lₚ
 open import Data.Product.Base using (_,_; _×_; ∃; ∃₂)
 open import Function.Base using (_∘_; _⟨_⟩_)
-open import Function.Equality using (_⟨$⟩_)
 open import Function.Inverse as Inv using (inverse)
 open import Level using (Level)
 open import Relation.Unary using (Pred)
diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
index 57233a7b2a..bc7af2193f 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
@@ -34,8 +34,6 @@ open import Data.Nat.Induction
 open import Data.Nat.Properties
 open import Data.Product.Base using (_,_; _×_; ∃; ∃₂; proj₁; proj₂)
 open import Function.Base using (_∘_; _⟨_⟩_; flip)
-open import Function.Equality using (_⟨$⟩_)
-open import Function.Inverse as Inv using (inverse)
 open import Level using (Level; _⊔_)
 open import Relation.Unary using (Pred; Decidable)
 open import Relation.Binary.Properties.Setoid S using (≉-resp₂)
diff --git a/src/Data/Product/Function/Dependent/Propositional.agda b/src/Data/Product/Function/Dependent/Propositional.agda
index b7333283ff..bde9e92c44 100644
--- a/src/Data/Product/Function/Dependent/Propositional.agda
+++ b/src/Data/Product/Function/Dependent/Propositional.agda
@@ -13,7 +13,7 @@ open import Data.Product.Base using (Σ; map; _,_)
 open import Data.Product.Function.NonDependent.Setoid
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Function.Base
-open import Function.Equality using (_⟶_; _⟨$⟩_)
+open import Function.Equality using (_⟨$⟩_)
 open import Function.Equivalence as Equiv using (_⇔_; module Equivalence)
 open import Function.HalfAdjointEquivalence using (↔→≃; _≃_)
 open import Function.Injection as Inj
diff --git a/src/Data/Product/Function/Dependent/Setoid/WithK.agda b/src/Data/Product/Function/Dependent/Setoid/WithK.agda
index 3336ecb5e5..3451200fb5 100644
--- a/src/Data/Product/Function/Dependent/Setoid/WithK.agda
+++ b/src/Data/Product/Function/Dependent/Setoid/WithK.agda
@@ -14,7 +14,7 @@ open import Data.Product.Function.Dependent.Setoid using (surjection)
 open import Data.Product.Relation.Binary.Pointwise.Dependent
 open import Relation.Binary
 open import Function.Base
-open import Function.Equality as F using (_⟶_; _⟨$⟩_)
+open import Function.Equality using (_⟨$⟩_)
 open import Function.Equivalence as Eq
   using (Equivalence; _⇔_; module Equivalence)
 open import Function.Injection as Inj
diff --git a/src/Data/Product/Function/NonDependent/Propositional.agda b/src/Data/Product/Function/NonDependent/Propositional.agda
index 7dfb28207d..a67490b8a5 100644
--- a/src/Data/Product/Function/NonDependent/Propositional.agda
+++ b/src/Data/Product/Function/NonDependent/Propositional.agda
@@ -12,7 +12,6 @@ module Data.Product.Function.NonDependent.Propositional where
 open import Data.Product.Base using (_×_; map)
 open import Data.Product.Function.NonDependent.Setoid
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
-open import Function.Equality using (_⟶_)
 open import Function.Equivalence as Eq using (_⇔_; module Equivalence)
 open import Function.Injection as Inj using (_↣_; module Injection)
 open import Function.Inverse as Inv using (_↔_; module Inverse)
diff --git a/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda b/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
index 16756bf375..a6ad0b2a39 100644
--- a/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
+++ b/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
@@ -13,7 +13,7 @@ open import Data.Product.Properties using (≡-dec)
 open import Data.Sum.Base
 open import Data.Unit.Base using (⊤)
 open import Function.Base
-open import Function.Equality as F using (_⟶_; _⟨$⟩_)
+open import Function.Equality using (_⟨$⟩_)
 open import Function.Equivalence as Eq
   using (Equivalence; _⇔_; module Equivalence)
 open import Function.Injection as Inj
diff --git a/src/Function/Endomorphism/Setoid.agda b/src/Function/Endomorphism/Setoid.agda
index d9890c3a35..a715ef5262 100644
--- a/src/Function/Endomorphism/Setoid.agda
+++ b/src/Function/Endomorphism/Setoid.agda
@@ -19,7 +19,7 @@ open import Agda.Builtin.Equality
 open import Algebra
 open import Algebra.Structures
 open import Algebra.Morphism; open Definitions
-open import Function.Equality
+open import Function.Equality using (setoid; _⟶_; id; _∘_; cong)
 open import Data.Nat.Base using (ℕ; _+_); open ℕ
 open import Data.Nat.Properties
 open import Data.Product.Base using (_,_)
diff --git a/src/Function/Indexed/Relation/Binary/Equality.agda b/src/Function/Indexed/Relation/Binary/Equality.agda
new file mode 100644
index 0000000000..ef9d6b3657
--- /dev/null
+++ b/src/Function/Indexed/Relation/Binary/Equality.agda
@@ -0,0 +1,27 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Function setoids and related constructions
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Function.Indexed.Relation.Binary.Equality where
+
+open import Relation.Binary 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
+
diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda
index 37c891312b..68a77807ad 100644
--- a/src/Relation/Binary/PropositionalEquality.agda
+++ b/src/Relation/Binary/PropositionalEquality.agda
@@ -11,7 +11,8 @@ module Relation.Binary.PropositionalEquality where
 import Axiom.Extensionality.Propositional as Ext
 open import Axiom.UniquenessOfIdentityProofs
 open import Function.Base using (id; _∘_)
-open import Function.Equality using (Π; _⟶_; ≡-setoid)
+open import Function.Equality using (Π; _⟶_)
+open import Function.Indexed.Relation.Binary.Equality using (≡-setoid)
 open import Level using (Level; _⊔_)
 open import Data.Product.Base using (∃)
 
diff --git a/src/Relation/Nullary/Universe.agda b/src/Relation/Nullary/Universe.agda
index 658f8c7bf7..3057b16eb6 100644
--- a/src/Relation/Nullary/Universe.agda
+++ b/src/Relation/Nullary/Universe.agda
@@ -22,7 +22,7 @@ open import Data.Sum.Relation.Binary.Pointwise
 open import Data.Product.Base as Prod hiding (map)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Function.Base using (_∘_; id)
-import Function.Equality as FunS
+open import Function.Indexed.Relation.Binary.Equality using (≡-setoid)
 open import Data.Empty
 open import Effect.Applicative
 open import Effect.Monad
@@ -53,7 +53,7 @@ mutual
   setoid (K P)     _ = PropEq.setoid P
   setoid (F₁ ∨ F₂) P = (setoid F₁ P) ⊎ₛ (setoid F₂ P)
   setoid (F₁ ∧ F₂) P = (setoid F₁ P) ×ₛ (setoid F₂ P)
-  setoid (P₁ ⇒ F₂) P = FunS.≡-setoid P₁
+  setoid (P₁ ⇒ F₂) P = ≡-setoid P₁
                          (Trivial.indexedSetoid (setoid F₂ P))
   setoid (¬¬ F)    P = Always.setoid (¬ ¬ ⟦ F ⟧ P) _