diff --git a/src/Algebra/Morphism/Construct/Terminal.agda b/src/Algebra/Morphism/Construct/Terminal.agda
index 227ebf2887..052b1a6cb5 100644
--- a/src/Algebra/Morphism/Construct/Terminal.agda
+++ b/src/Algebra/Morphism/Construct/Terminal.agda
@@ -20,7 +20,7 @@ open import Algebra.Bundles.Raw
 open import Algebra.Morphism.Structures
 
 open import Data.Product.Base using (_,_)
-open import Function.Definitions using (StrictlySurjective)
+open import Function.Definitions.Strict using (StrictlySurjective)
 import Relation.Binary.Morphism.Definitions as Rel
 open import Relation.Binary.Morphism.Structures
 
diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index 794b93f76b..667b5da5e7 100644
--- a/src/Data/Fin/Permutation.agda
+++ b/src/Data/Fin/Permutation.agda
@@ -20,7 +20,7 @@ open import Function.Bundles using (_↔_; Injection; Inverse; mk↔ₛ′)
 open import Function.Construct.Composition using (_↔-∘_)
 open import Function.Construct.Identity using (↔-id)
 open import Function.Construct.Symmetry using (↔-sym)
-open import Function.Definitions using (StrictlyInverseˡ; StrictlyInverseʳ)
+open import Function.Definitions.Strict using (StrictlyInverseˡ; StrictlyInverseʳ)
 open import Function.Properties.Inverse using (↔⇒↣)
 open import Function.Base using (_∘_)
 open import Level using (0ℓ)
diff --git a/src/Data/Product/Function/Dependent/Propositional.agda b/src/Data/Product/Function/Dependent/Propositional.agda
index 4c6f391e2f..0c2d28423d 100644
--- a/src/Data/Product/Function/Dependent/Propositional.agda
+++ b/src/Data/Product/Function/Dependent/Propositional.agda
@@ -23,7 +23,8 @@ open import Function.Properties.Inverse.HalfAdjointEquivalence
   using (↔⇒≃; _≃_; ≃⇒↔)
 open import Function.Consequences.Propositional
   using (inverseʳ⇒injective; strictlySurjective⇒surjective)
-open import Function.Definitions using (Inverseˡ; Inverseʳ; Injective; StrictlySurjective)
+open import Function.Definitions using (Inverseˡ; Inverseʳ; Injective)
+open import Function.Definitions.Strict using (StrictlySurjective)
 open import Function.Bundles
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 open import Relation.Binary.PropositionalEquality.Properties as ≡
diff --git a/src/Data/Sum/Function/Setoid.agda b/src/Data/Sum/Function/Setoid.agda
index 659bad1ef3..e9815e3e04 100644
--- a/src/Data/Sum/Function/Setoid.agda
+++ b/src/Data/Sum/Function/Setoid.agda
@@ -15,6 +15,7 @@ open import Relation.Binary
 open import Function.Base
 open import Function.Bundles
 open import Function.Definitions
+open import Function.Definitions.Strict
 open import Level
 
 private
diff --git a/src/Function.agda b/src/Function.agda
index b4155ef8ef..911824a0a2 100644
--- a/src/Function.agda
+++ b/src/Function.agda
@@ -12,6 +12,7 @@ open import Function.Core public
 open import Function.Base public
 open import Function.Strict public
 open import Function.Definitions public
+open import Function.Definitions.Strict public
 open import Function.Structures public
 open import Function.Structures.Biased public
 open import Function.Bundles public
diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda
index 6532715a21..aa0df54302 100644
--- a/src/Function/Bundles.agda
+++ b/src/Function/Bundles.agda
@@ -21,6 +21,7 @@ module Function.Bundles where
 
 open import Function.Base using (_∘_)
 open import Function.Definitions
+open import Function.Definitions.Strict
 import Function.Structures as FunctionStructures
 open import Level using (Level; _⊔_; suc)
 open import Data.Product.Base using (_,_; proj₁; proj₂)
diff --git a/src/Function/Consequences.agda b/src/Function/Consequences.agda
index 2a13d452f6..f497c3a8f5 100644
--- a/src/Function/Consequences.agda
+++ b/src/Function/Consequences.agda
@@ -12,6 +12,7 @@ module Function.Consequences where
 
 open import Data.Product.Base as Product
 open import Function.Definitions
+open import Function.Definitions.Strict
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (Setoid)
@@ -104,11 +105,12 @@ inverseʳ⇒strictlyInverseʳ : ∀ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ
                             Reflexive ≈₂ →
                             Inverseʳ ≈₁ ≈₂ f f⁻¹ →
                             StrictlyInverseʳ ≈₁ f f⁻¹
-inverseʳ⇒strictlyInverseʳ _ _ refl sinv x = sinv refl
+inverseʳ⇒strictlyInverseʳ {f = f} {f⁻¹ = f⁻¹} ≈₁ ≈₂ =
+  inverseˡ⇒strictlyInverseˡ {f = f⁻¹} {f⁻¹ = f} ≈₂ ≈₁
 
 strictlyInverseʳ⇒inverseʳ : Transitive ≈₁ →
                             Congruent ≈₂ ≈₁ f⁻¹ →
                             StrictlyInverseʳ ≈₁ f f⁻¹ →
                             Inverseʳ ≈₁ ≈₂ f f⁻¹
-strictlyInverseʳ⇒inverseʳ trans cong sinv {x} y≈f⁻¹x =
-  trans (cong y≈f⁻¹x) (sinv x)
+strictlyInverseʳ⇒inverseʳ {≈₁ = ≈₁} {≈₂ = ≈₂} {f⁻¹ = f⁻¹} {f = f} =
+  strictlyInverseˡ⇒inverseˡ {≈₂ = ≈₁} {≈₁ = ≈₂} {f = f⁻¹} {f⁻¹ = f}
diff --git a/src/Function/Consequences/Propositional.agda b/src/Function/Consequences/Propositional.agda
index a2558a9c48..92609529a7 100644
--- a/src/Function/Consequences/Propositional.agda
+++ b/src/Function/Consequences/Propositional.agda
@@ -14,7 +14,8 @@ module Function.Consequences.Propositional
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; cong)
 open import Relation.Binary.PropositionalEquality.Properties
   using (setoid)
-open import Function.Definitions
+import Function.Definitions as Definitions
+open import Function.Definitions.Strict as Strict
 open import Relation.Nullary.Negation.Core using (contraposition)
 
 import Function.Consequences.Setoid (setoid A) (setoid B) as Setoid
@@ -37,17 +38,19 @@ private
     f : A → B
     f⁻¹ : B → A
 
+open Definitions (_≡_ {A = A}) (_≡_ {A = B})
+
 strictlySurjective⇒surjective : StrictlySurjective _≡_ f →
-                                 Surjective _≡_ _≡_ f
+                                 Surjective f
 strictlySurjective⇒surjective =
  Setoid.strictlySurjective⇒surjective (cong _)
 
 strictlyInverseˡ⇒inverseˡ : ∀ f → StrictlyInverseˡ _≡_ f f⁻¹ →
-                            Inverseˡ _≡_ _≡_ f f⁻¹
+                            Inverseˡ f f⁻¹
 strictlyInverseˡ⇒inverseˡ f =
   Setoid.strictlyInverseˡ⇒inverseˡ (cong _)
 
 strictlyInverseʳ⇒inverseʳ : ∀ f → StrictlyInverseʳ _≡_ f f⁻¹ →
-                            Inverseʳ _≡_ _≡_ f f⁻¹
+                            Inverseʳ f f⁻¹
 strictlyInverseʳ⇒inverseʳ f =
   Setoid.strictlyInverseʳ⇒inverseʳ (cong _)
diff --git a/src/Function/Consequences/Setoid.agda b/src/Function/Consequences/Setoid.agda
index d2c3b948d9..d310c7795f 100644
--- a/src/Function/Consequences/Setoid.agda
+++ b/src/Function/Consequences/Setoid.agda
@@ -16,6 +16,7 @@ module Function.Consequences.Setoid
   where
 
 open import Function.Definitions
+open import Function.Definitions.Strict
 open import Relation.Nullary.Negation.Core
 
 import Function.Consequences as C
diff --git a/src/Function/Definitions.agda b/src/Function/Definitions.agda
index 225dc53998..6b7b49da9c 100644
--- a/src/Function/Definitions.agda
+++ b/src/Function/Definitions.agda
@@ -1,64 +1,43 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Definitions for types of functions.
+-- Definitions for types of functions,
+-- wrt to `_≈₁_` equality over the domain
+-- and `_≈₂_` equality over the codomain.
 ------------------------------------------------------------------------
 
 -- The contents of this file should usually be accessed from `Function`.
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-module Function.Definitions where
-
-open import Data.Product.Base using (∃; _×_)
-open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 
-private
-  variable
-    a ℓ₁ ℓ₂ : Level
-    A B : Set a
-
-------------------------------------------------------------------------
--- Basic definitions
-
-module _
-  (_≈₁_ : Rel A ℓ₁) -- Equality over the domain
-  (_≈₂_ : Rel B ℓ₂) -- Equality over the codomain
+module Function.Definitions
+  {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂)
   where
 
-  Congruent : (A → B) → Set _
-  Congruent f = ∀ {x y} → x ≈₁ y → f x ≈₂ f y
-
-  Injective : (A → B) → Set _
-  Injective f = ∀ {x y} → f x ≈₂ f y → x ≈₁ y
-
-  Surjective : (A → B) → Set _
-  Surjective f = ∀ y → ∃ λ x → ∀ {z} → z ≈₁ x → f z ≈₂ y
-
-  Bijective : (A → B) → Set _
-  Bijective f = Injective f × Surjective f
+open import Data.Product.Base using (∃; _×_)
 
-  Inverseˡ : (A → B) → (B → A) → Set _
-  Inverseˡ f g = ∀ {x y} → y ≈₁ g x → f y ≈₂ x
+------------------------------------------------------------------------
+-- Basic definitions
 
-  Inverseʳ : (A → B) → (B → A) → Set _
-  Inverseʳ f g = ∀ {x y} → y ≈₂ f x → g y ≈₁ x
+Congruent : (A → B) → Set _
+Congruent f = ∀ {x y} → x ≈₁ y → f x ≈₂ f y
 
-  Inverseᵇ : (A → B) → (B → A) → Set _
-  Inverseᵇ f g = Inverseˡ f g × Inverseʳ f g
+Injective : (A → B) → Set _
+Injective f = ∀ {x y} → f x ≈₂ f y → x ≈₁ y
 
-------------------------------------------------------------------------
--- Strict definitions
+Surjective : (A → B) → Set _
+Surjective f = ∀ y → ∃ λ x → ∀ {z} → z ≈₁ x → f z ≈₂ y
 
--- These are often easier to use once but much harder to compose and
--- reason about.
+Bijective : (A → B) → Set _
+Bijective f = Injective f × Surjective f
 
-StrictlySurjective : Rel B ℓ₂ → (A → B) → Set _
-StrictlySurjective _≈₂_ f = ∀ y → ∃ λ x → f x ≈₂ y
+Inverseˡ : (A → B) → (B → A) → Set _
+Inverseˡ f g = ∀ {x y} → y ≈₁ g x → f y ≈₂ x
 
-StrictlyInverseˡ : Rel B ℓ₂ → (A → B) → (B → A) → Set _
-StrictlyInverseˡ _≈₂_ f g = ∀ y → f (g y) ≈₂ y
+Inverseʳ : (A → B) → (B → A) → Set _
+Inverseʳ f g = ∀ {x y} → y ≈₂ f x → g y ≈₁ x
 
-StrictlyInverseʳ : Rel A ℓ₁ → (A → B) → (B → A) → Set _
-StrictlyInverseʳ _≈₁_ f g = ∀ x → g (f x) ≈₁ x
+Inverseᵇ : (A → B) → (B → A) → Set _
+Inverseᵇ f g = Inverseˡ f g × Inverseʳ f g
diff --git a/src/Function/Definitions/Strict.agda b/src/Function/Definitions/Strict.agda
new file mode 100644
index 0000000000..4a2adfb7dc
--- /dev/null
+++ b/src/Function/Definitions/Strict.agda
@@ -0,0 +1,37 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definitions for types of functions.
+------------------------------------------------------------------------
+
+-- The contents of this file should usually be accessed from `Function`.
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Core using (Rel)
+
+module Function.Definitions.Strict {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) where
+
+open import Data.Product.Base using (∃)
+open import Level using (Level)
+
+private
+  variable
+    b : Level
+    B : Set b
+
+------------------------------------------------------------------------
+-- Strict definitions
+
+-- These are often easier to use once but much harder to compose and
+-- reason about.
+
+StrictlySurjective : (B → A) → Set _
+StrictlySurjective f = ∀ y → ∃ λ x → f x ≈ y
+
+StrictlyInverseˡ : (B → A) → (A → B) → Set _
+StrictlyInverseˡ f g = ∀ y → f (g y) ≈ y
+
+StrictlyInverseʳ : (A → B) → (B → A) → Set _
+StrictlyInverseʳ g f = StrictlyInverseˡ f g
+
diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda
index 9533cfb179..af556a955a 100644
--- a/src/Function/Structures.agda
+++ b/src/Function/Structures.agda
@@ -20,6 +20,7 @@ module Function.Structures {a b ℓ₁ ℓ₂}
 open import Data.Product.Base as Product using (∃; _×_; _,_)
 open import Function.Base
 open import Function.Definitions
+open import Function.Definitions.Strict
 open import Level using (_⊔_)
 
 ------------------------------------------------------------------------
diff --git a/src/Function/Structures/Biased.agda b/src/Function/Structures/Biased.agda
index e25c4970c9..b47a00cf21 100644
--- a/src/Function/Structures/Biased.agda
+++ b/src/Function/Structures/Biased.agda
@@ -21,6 +21,7 @@ module Function.Structures.Biased {a b ℓ₁ ℓ₂}
 open import Data.Product.Base as Product using (∃; _×_; _,_)
 open import Function.Base
 open import Function.Definitions
+open import Function.Definitions.Strict
 open import Function.Structures _≈₁_ _≈₂_
 open import Function.Consequences.Setoid
 open import Level using (_⊔_)