Function setoid is back. (#2240)

* Function setoid is back.

* make all changes asked for in review

* fix indentation

CHANGELOG.md

@@ -48,18 +48,26 @@ Deprecated names
 
 New modules
 -----------
-
-* Symmetric interior of a binary relation
- ```
- Relation.Binary.Construct.Interior.Symmetric
- ```
-
 * `Algebra.Module.Bundles.Raw`: raw bundles for module-like algebraic structures
 
 * Nagata's construction of the "idealization of a module":
  ```agda
  Algebra.Module.Construct.Idealization
  ```
+
+* `Function.Relation.Binary.Equality`
+ ```agda
+ setoid : Setoid a₁ a₂ → Setoid b₁ b₂ → Setoid _ _
+ ```
+ and a convenient infix version
+ ```agda
+ _⇨_ = setoid
+ ```
+
+* Symmetric interior of a binary relation
+ ```
+ Relation.Binary.Construct.Interior.Symmetric
+ ```
 
 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