Refine some Function.Equality imports

src/Function/Equality.agda

@@ -11,6 +11,7 @@
 -- `Bijection`. The alternative definitions found in this file will
 -- eventually be deprecated.
 
+-- check if modules are actually using Function.Equality and port them
 module Function.Equality where
 
 import Function.Base as Fun
@@ -24,6 +25,7 @@ import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial
 ------------------------------------------------------------------------
 -- Functions which preserve equality
 
+-- indexed
 record Π {f₁ f₂ t₁ t₂}
  (From : Setoid f₁ f₂)
  (To : IndexedSetoid (Setoid.Carrier From) t₁ t₂) :
@@ -37,6 +39,7 @@ open Π public
 
 infixr 0 _⟶_
 
+-- not indexed
 _⟶_ : ∀ {f₁ f₂ t₁ t₂} → Setoid f₁ f₂ → Setoid t₁ t₂ → Set _
 From ⟶ To = Π From (Trivial.indexedSetoid To)
 
@@ -72,6 +75,7 @@ const {B = B} b = record
 
 -- Dependent.
 
+-- indexed
 setoid : ∀ {f₁ f₂ t₁ t₂}
  (From : Setoid f₁ f₂) →
  IndexedSetoid (Setoid.Carrier From) t₁ t₂ →
@@ -91,6 +95,7 @@ setoid From To = record
 
 -- Non-dependent.
 
+-- no indexed
 infixr 0 _⇨_
 
 _⇨_ : ∀ {f₁ f₂ t₁ t₂} → Setoid f₁ f₂ → Setoid t₁ t₂ → Setoid _ _
@@ -99,6 +104,7 @@ From ⇨ To = setoid From (Trivial.indexedSetoid To)
 -- A variant of setoid which uses the propositional equality setoid
 -- for the domain, and a more convenient definition of _≈_.
 
+-- indexed
 ≡-setoid : ∀ {f t₁ t₂} (From : Set f) → IndexedSetoid From t₁ t₂ → Setoid _ _
 ≡-setoid From To = record
  { Carrier = (x : From) → Carrier x

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