Function setoid is back.

CHANGELOG.md

@@ -45,13 +45,22 @@ Deprecated names
 
 New modules
 -----------
-
+  
 * `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
+  ```
 
 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