Move ≡-setoid to Function.Indexed.Relation.Binary.Equality (#2047)

Author: Saransh-cpp

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)

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

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

src/Data/Product/Function/Dependent/Setoid/WithK.agda

@@ -13,7 +13,7 @@ open import Data.Product.Base using (_,_)
 open import Data.Product.Function.Dependent.Setoid using (surjection)
 open import Data.Product.Relation.Binary.Pointwise.Dependent
 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

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)

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

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 (_,_)

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
+

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 (∃)
 

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