Function setoid is back.

CHANGELOG.md

@@ -29,6 +29,15 @@ Deprecated names
 New modules
 -----------
 
+* `Function.Relation.Binary.Equality`
+  ```agda
+  setoid : Setoid a₁ a₂ → Setoid b₁ b₂ → Setoid _ _
+  ```
+  and a convenient infix version
+  ```agda
+  _⇨_ = setoid
+  ```
+
 Additions to existing modules
 -----------------------------
 

src/Function/Relation/Binary/Setoid/Equality.agda

@@ -0,0 +1,50 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Function Equality setoid
+------------------------------------------------------------------------
+
+{-# 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)
+
+  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
+
+  setoid : Setoid _ _
+  setoid = record
+    { Carrier = Func From To
+    ; _≈_ = _≈_
+    ; isEquivalence = record  -- need to η-expand else Agda gets confused
+      { refl = λ {f} → refl {f}
+      ; sym = λ {f} {g} → sym {f} {g}
+      ; trans = λ {f} {g} {h} → trans {f} {g} {h}
+      }
+    }
+
+  -- most of the time, this infix version is nicer to use
+  infixr 9 _⇨_
+  _⇨_ : Setoid _ _
+  _⇨_ = setoid