Removed module parameters from Function (#977)

Author: MatthewDaggitt

src/Function.agda

@@ -6,20 +6,9 @@
 
 {-# OPTIONS --without-K --safe #-}
 
--- Note that it is not necessary to provide the equality relations. If
--- they are not provided then it is necessary to provide them directly
--- when using the contents of `Function.Definitions` and
--- `Function.Structures`.
-
-open import Relation.Binary using (Rel)
-
-module Function
-  {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
-  (_≈₁_ : Rel A ℓ₁) -- Equality over the domain
-  (_≈₂_ : Rel B ℓ₂) -- Equality over the codomain
-  where
+module Function where
 
 open import Function.Core public
-open import Function.Definitions _≈₁_ _≈₂_ public
-open import Function.Structures  _≈₁_ _≈₂_ public
+open import Function.Definitions public
+open import Function.Structures public
 open import Function.Bundles public

src/Function/Construct/Composition.agda

@@ -82,28 +82,28 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {≈₃ : Rel C ℓ₃}
     { cong           = G.cong ∘ F.cong
     ; isEquivalence₁ = F.isEquivalence₁
     ; isEquivalence₂ = G.isEquivalence₂
-    } where module F = IsCongruent _ _ f-cong; module G = IsCongruent _ _ g-cong
+    } where module F = IsCongruent f-cong; module G = IsCongruent g-cong
 
   isInjection : IsInjection ≈₁ ≈₂ f → IsInjection ≈₂ ≈₃ g →
                 IsInjection ≈₁ ≈₃ (g ∘ f)
   isInjection f-inj g-inj = record
     { isCongruent = isCongruent F.isCongruent G.isCongruent
     ; injective   = injective ≈₁ ≈₂ ≈₃ F.injective G.injective
-    } where module F = IsInjection _ _ f-inj; module G = IsInjection _ _ g-inj
+    } where module F = IsInjection f-inj; module G = IsInjection g-inj
 
   isSurjection : IsSurjection ≈₁ ≈₂ f → IsSurjection ≈₂ ≈₃ g →
                  IsSurjection ≈₁ ≈₃ (g ∘ f)
   isSurjection f-surj g-surj = record
     { isCongruent = isCongruent F.isCongruent G.isCongruent
     ; surjective   = surjective ≈₁ ≈₂ ≈₃ G.Eq₂.trans G.cong F.surjective G.surjective
-    } where module F = IsSurjection _ _ f-surj; module G = IsSurjection _ _ g-surj
+    } where module F = IsSurjection f-surj; module G = IsSurjection g-surj
 
   isBijection : IsBijection ≈₁ ≈₂ f → IsBijection ≈₂ ≈₃ g →
                 IsBijection ≈₁ ≈₃ (g ∘ f)
   isBijection f-bij g-bij = record
     { isInjection = isInjection F.isInjection G.isInjection
     ; surjective  = surjective ≈₁ ≈₂ ≈₃ G.Eq₂.trans G.cong F.surjective G.surjective
-    } where module F = IsBijection _ _ f-bij; module G = IsBijection _ _ g-bij
+    } where module F = IsBijection f-bij; module G = IsBijection g-bij
 
 module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {≈₃ : Rel C ℓ₃}
          {f : A → B} {g : B → C} {f⁻¹ : B → A} {g⁻¹ : C → B}
@@ -115,22 +115,22 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {≈₃ : Rel C ℓ₃}
     { isCongruent = isCongruent F.isCongruent G.isCongruent
     ; cong₂       = congruent ≈₃ ≈₂ ≈₁ G.cong₂ F.cong₂
     ; inverseˡ    = inverseˡ ≈₁ ≈₂ ≈₃ f _ G.Eq₂.trans G.cong₁ F.inverseˡ G.inverseˡ
-    } where module F = IsLeftInverse _ _ f-invˡ; module G = IsLeftInverse _ _ g-invˡ
+    } where module F = IsLeftInverse f-invˡ; module G = IsLeftInverse g-invˡ
 
   isRightInverse : IsRightInverse ≈₁ ≈₂ f f⁻¹ → IsRightInverse ≈₂ ≈₃ g g⁻¹ →
                    IsRightInverse ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
   isRightInverse f-invʳ g-invʳ = record
     { isCongruent = isCongruent F.isCongruent G.isCongruent
     ; cong₂       = congruent ≈₃ ≈₂ ≈₁ G.cong₂ F.cong₂
     ; inverseʳ    = inverseʳ ≈₁ ≈₂ ≈₃ _ g⁻¹ F.Eq₁.trans F.cong₂ F.inverseʳ G.inverseʳ
-    } where module F = IsRightInverse _ _ f-invʳ; module G = IsRightInverse _ _ g-invʳ
+    } where module F = IsRightInverse f-invʳ; module G = IsRightInverse g-invʳ
 
   isInverse : IsInverse ≈₁ ≈₂ f f⁻¹ → IsInverse ≈₂ ≈₃ g g⁻¹ →
               IsInverse ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
   isInverse f-inv g-inv = record
     { isLeftInverse = isLeftInverse F.isLeftInverse G.isLeftInverse
     ; inverseʳ      = inverseʳ ≈₁ ≈₂ ≈₃ _ g⁻¹ F.Eq₁.trans F.cong₂ F.inverseʳ G.inverseʳ
-    } where module F = IsInverse _ _ f-inv; module G = IsInverse _ _ g-inv
+    } where module F = IsInverse f-inv; module G = IsInverse g-inv
 
 ------------------------------------------------------------------------
 -- Setoid bundles

src/Function/Construct/Identity.agda

@@ -9,7 +9,10 @@
 module Function.Construct.Identity where
 
 open import Data.Product using (_,_)
-import Function
+open import Function using (id)
+open import Function.Bundles
+import Function.Definitions as Definitions
+import Function.Structures as Structures
 open import Level
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality using (_≡_; setoid)
@@ -24,7 +27,7 @@ private
 
 module _ (_≈_ : Rel A ℓ) where
 
-  open Function _≈_ _≈_
+  open Definitions _≈_ _≈_
 
   injective : Injective id
   injective = id
@@ -49,7 +52,7 @@ module _ (_≈_ : Rel A ℓ) where
 
 module _ {_≈_ : Rel A ℓ} (isEq : IsEquivalence _≈_) where
 
-  open Function _≈_ _≈_
+  open Structures _≈_ _≈_
   open IsEquivalence isEq
 
   isCongruent : IsCongruent id
@@ -103,7 +106,6 @@ module _ {_≈_ : Rel A ℓ} (isEq : IsEquivalence _≈_) where
 module _ (S : Setoid a ℓ) where
 
   open Setoid S
-  open Function _≈_ _≈_
 
   injection : Injection S S
   injection = record
@@ -166,8 +168,6 @@ module _ (S : Setoid a ℓ) where
 
 module _ (A : Set a) where
 
-  open Function {A = A} {A} _≡_ _≡_
-
   id-↣ : A ↣ A
   id-↣ = injection (setoid A)