diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8e74556b52..b7cb6aa60b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -272,7 +272,7 @@ Non-backwards compatible changes
 * Added new aliases `Is(Meet/Join)(Bounded)Semilattice` for `Is(Bounded)Semilattice`
   which can be used to indicate meet/join-ness of the original structures.
 
-#### Function hierarchy
+#### Removal of the old function hierarchy
 
 * The switch to the new function hierarchy is complete and the following definitions
   now use the new definitions instead of the old ones:
@@ -345,9 +345,41 @@ Non-backwards compatible changes
   * `Relation.Nullary.Decidable`
     * `map`
 
-* The names of the fields in the records of the new hierarchy have been
-  changed from `f`, `g`, `cong₁`, `cong₂` to `to`, `from`, `to-cong`, `from-cong`.
 
+#### Changes to the new function hierarchy
+
+* The names of the fields in `Function.Bundles` have been
+  changed from `f`, `g`, `cong₁` and `cong₂` to `to`, `from`, `to-cong`, `from-cong`.
+
+* The module `Function.Definitions` no longer has two equalities as module arguments, as
+  they did not interact as intended with the re-exports from `Function.Definitions.(Core1/Core2)`.
+  The latter have been removed and their definitions folded into `Function.Definitions`.
+  
+* In `Function.Definitions` the types of `Surjective`, `Injective` and `Surjective` 
+  have been changed from:
+  ```
+  Surjective f = ∀ y → ∃ λ x → f x ≈₂ y
+  Inverseˡ f g = ∀ y → f (g y) ≈₂ y
+  Inverseʳ f g = ∀ x → g (f x) ≈₁ x
+  ```
+  to:
+  ```
+  Surjective f = ∀ y → ∃ λ x → ∀ {z} → z ≈₁ x → f z ≈₂ y
+  Inverseˡ f g = ∀ {x y} → y ≈₁ g x → f y ≈₂ x
+  Inverseʳ f g = ∀ {x y} → y ≈₂ f x → g y ≈₁ x
+  ```
+  This is for several reasons: i) the new definitions compose much more easily, ii) Agda
+  can better infer the equalities used.
+  
+  To ease backwards compatibility:
+   - the old definitions have been moved to the new names  `StrictlySurjective`, 
+	 `StrictlyInverseˡ` and `StrictlyInverseʳ`. 
+   - The records in  `Function.Structures` and `Function.Bundles` export proofs 
+	 of these under the names `strictlySurjective`, `strictlyInverseˡ` and 
+	 `strictlyInverseʳ`,
+   - Conversion functions have been added in both directions to
+	 `Function.Consequences(.Propositional)`. 
+  
 #### Proofs of non-zeroness/positivity/negativity as instance arguments
 
 * Many numeric operations in the library require their arguments to be non-zero,
@@ -2206,6 +2238,9 @@ Other minor changes
 * Added a new proof to `Data.Nat.Binary.Properties`:
   ```agda
   suc-injective : Injective _≡_ _≡_ suc
+  toℕ-inverseˡ  : Inverseˡ _≡_ _≡_ toℕ fromℕ
+  toℕ-inverseʳ  : Inverseʳ _≡_ _≡_ toℕ fromℕ
+  toℕ-inverseᵇ  : Inverseᵇ _≡_ _≡_ toℕ fromℕ
   ```
 
 * Added a new pattern synonym to `Data.Nat.Divisibility.Core`:
diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda
index f5cac63048..1aa2b8f4c8 100644
--- a/src/Algebra/Consequences/Setoid.agda
+++ b/src/Algebra/Consequences/Setoid.agda
@@ -19,8 +19,8 @@ open import Algebra.Core
 open import Algebra.Definitions _≈_
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Product.Base using (_,_)
-open import Function.Base using (_$_)
-import Function.Definitions as FunDefs
+open import Function.Base using (_$_; id; _∘_)
+open import Function.Definitions
 import Relation.Binary.Consequences as Bin
 open import Relation.Binary.Reasoning.Setoid S
 open import Relation.Unary using (Pred)
@@ -67,45 +67,32 @@ module _ {_•_ : Op₂ A} (cong : Congruent₂ _•_) where
     y • x             ∎
 
 ------------------------------------------------------------------------
--- Involutive/SelfInverse functions
-
-module _ {f : Op₁ A} (inv : Involutive f) where
-
-  open FunDefs _≈_ _≈_
-
-  involutive⇒surjective : Surjective f
-  involutive⇒surjective y = f y , inv y
+-- SelfInverse
 
 module _ {f : Op₁ A} (self : SelfInverse f) where
 
   selfInverse⇒involutive : Involutive f
   selfInverse⇒involutive = reflexive+selfInverse⇒involutive _≈_ refl self
 
-  private
-
-    inv = selfInverse⇒involutive
-
-  open FunDefs _≈_ _≈_
-
-  selfInverse⇒congruent : Congruent f
+  selfInverse⇒congruent : Congruent _≈_ _≈_ f
   selfInverse⇒congruent {x} {y} x≈y = sym (self (begin
-    f (f x) ≈⟨ inv x ⟩
+    f (f x) ≈⟨ selfInverse⇒involutive x ⟩
     x       ≈⟨ x≈y ⟩
     y       ∎))
 
-  selfInverse⇒inverseᵇ : Inverseᵇ f f
-  selfInverse⇒inverseᵇ = inv , inv
+  selfInverse⇒inverseᵇ : Inverseᵇ _≈_ _≈_ f f
+  selfInverse⇒inverseᵇ = self ∘ sym , self ∘ sym
 
-  selfInverse⇒surjective : Surjective f
-  selfInverse⇒surjective = involutive⇒surjective inv
+  selfInverse⇒surjective : Surjective _≈_ _≈_ f
+  selfInverse⇒surjective y = f y , self ∘ sym
 
-  selfInverse⇒injective : Injective f
+  selfInverse⇒injective : Injective _≈_ _≈_ f
   selfInverse⇒injective {x} {y} x≈y = begin
     x       ≈˘⟨ self x≈y ⟩
-    f (f y) ≈⟨ inv y ⟩
+    f (f y) ≈⟨ selfInverse⇒involutive y ⟩
     y       ∎
 
-  selfInverse⇒bijective : Bijective f
+  selfInverse⇒bijective : Bijective _≈_ _≈_ f
   selfInverse⇒bijective = selfInverse⇒injective , selfInverse⇒surjective
 
 ------------------------------------------------------------------------
diff --git a/src/Algebra/Lattice/Morphism/Construct/Composition.agda b/src/Algebra/Lattice/Morphism/Construct/Composition.agda
index 42f609c8de..fe5266af3d 100644
--- a/src/Algebra/Lattice/Morphism/Construct/Composition.agda
+++ b/src/Algebra/Lattice/Morphism/Construct/Composition.agda
@@ -57,5 +57,5 @@ module _ {L₁ : RawLattice a ℓ₁}
     → IsLatticeIsomorphism L₁ L₃ (g ∘ f)
   isLatticeIsomorphism f-iso g-iso = record
     { isLatticeMonomorphism = isLatticeMonomorphism F.isLatticeMonomorphism G.isLatticeMonomorphism
-    ; surjective            = Func.surjective (_≈_ L₁) _ _ ≈₃-trans G.⟦⟧-cong F.surjective G.surjective
+    ; surjective            = Func.surjective _ _ (_≈_ L₃) F.surjective G.surjective
     } where module F = IsLatticeIsomorphism f-iso; module G = IsLatticeIsomorphism g-iso
diff --git a/src/Algebra/Lattice/Morphism/Construct/Identity.agda b/src/Algebra/Lattice/Morphism/Construct/Identity.agda
index 8531643540..5fba1b976b 100644
--- a/src/Algebra/Lattice/Morphism/Construct/Identity.agda
+++ b/src/Algebra/Lattice/Morphism/Construct/Identity.agda
@@ -13,6 +13,7 @@ open import Algebra.Lattice.Morphism.Structures
   using ( module LatticeMorphisms )
 open import Data.Product.Base using (_,_)
 open import Function.Base using (id)
+import Function.Construct.Identity as Id
 open import Level using (Level)
 open import Relation.Binary.Morphism.Construct.Identity using (isRelHomomorphism)
 open import Relation.Binary.Definitions using (Reflexive)
@@ -40,5 +41,5 @@ module _ (L : RawLattice c ℓ) (open RawLattice L) (refl : Reflexive _≈_) whe
   isLatticeIsomorphism : IsLatticeIsomorphism id
   isLatticeIsomorphism = record
     { isLatticeMonomorphism = isLatticeMonomorphism
-    ; surjective = _, refl
+    ; surjective = Id.surjective _
     }
diff --git a/src/Algebra/Lattice/Morphism/Structures.agda b/src/Algebra/Lattice/Morphism/Structures.agda
index 7e7c34c163..87cf92e616 100644
--- a/src/Algebra/Lattice/Morphism/Structures.agda
+++ b/src/Algebra/Lattice/Morphism/Structures.agda
@@ -12,7 +12,7 @@ open import Algebra.Morphism
 open import Algebra.Lattice.Bundles
 import Algebra.Morphism.Definitions as MorphismDefinitions
 open import Level using (Level; _⊔_)
-import Function.Definitions as FunctionDefinitions
+open import Function.Definitions
 open import Relation.Binary.Morphism.Structures
 open import Relation.Binary.Core
 
@@ -44,7 +44,6 @@ module LatticeMorphisms (L₁ : RawLattice a ℓ₁) (L₂ : RawLattice b ℓ₂
   module ∧ = MagmaMorphisms ∧-rawMagma₁ ∧-rawMagma₂
 
   open MorphismDefinitions A B _≈₂_
-  open FunctionDefinitions _≈₁_ _≈₂_
 
 
   record IsLatticeHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
@@ -71,7 +70,7 @@ module LatticeMorphisms (L₁ : RawLattice a ℓ₁) (L₂ : RawLattice b ℓ₂
   record IsLatticeMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isLatticeHomomorphism : IsLatticeHomomorphism ⟦_⟧
-      injective             : Injective ⟦_⟧
+      injective             : Injective _≈₁_ _≈₂_ ⟦_⟧
 
     open IsLatticeHomomorphism isLatticeHomomorphism public
 
@@ -94,7 +93,7 @@ module LatticeMorphisms (L₁ : RawLattice a ℓ₁) (L₂ : RawLattice b ℓ₂
   record IsLatticeIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isLatticeMonomorphism : IsLatticeMonomorphism ⟦_⟧
-      surjective            : Surjective ⟦_⟧
+      surjective            : Surjective _≈₁_ _≈₂_ ⟦_⟧
 
     open IsLatticeMonomorphism isLatticeMonomorphism public
 
diff --git a/src/Algebra/Module/Morphism/Construct/Composition.agda b/src/Algebra/Module/Morphism/Construct/Composition.agda
index 3aeb7a5f26..8c39496dd4 100644
--- a/src/Algebra/Module/Morphism/Construct/Composition.agda
+++ b/src/Algebra/Module/Morphism/Construct/Composition.agda
@@ -51,7 +51,7 @@ module _
                                 IsLeftSemimoduleIsomorphism M₁ M₃ (g ∘ f)
   isLeftSemimoduleIsomorphism f-iso g-iso = record
     { isLeftSemimoduleMonomorphism = isLeftSemimoduleMonomorphism F.isLeftSemimoduleMonomorphism G.isLeftSemimoduleMonomorphism
-    ; surjective                   = Func.surjective (_≈ᴹ_ M₁) _ _ (≈ᴹ-trans M₃) G.⟦⟧-cong F.surjective G.surjective
+    ; surjective                   = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective
     } where module F = IsLeftSemimoduleIsomorphism f-iso; module G = IsLeftSemimoduleIsomorphism g-iso
 
 module _
@@ -85,7 +85,7 @@ module _
                             IsLeftModuleIsomorphism M₁ M₃ (g ∘ f)
   isLeftModuleIsomorphism f-iso g-iso = record
     { isLeftModuleMonomorphism = isLeftModuleMonomorphism F.isLeftModuleMonomorphism G.isLeftModuleMonomorphism
-    ; surjective               = Func.surjective (_≈ᴹ_ M₁) _ _ (≈ᴹ-trans M₃) G.⟦⟧-cong F.surjective G.surjective
+    ; surjective               = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective
     } where module F = IsLeftModuleIsomorphism f-iso; module G = IsLeftModuleIsomorphism g-iso
 
 module _
@@ -119,7 +119,7 @@ module _
                                  IsRightSemimoduleIsomorphism M₁ M₃ (g ∘ f)
   isRightSemimoduleIsomorphism f-iso g-iso = record
     { isRightSemimoduleMonomorphism = isRightSemimoduleMonomorphism F.isRightSemimoduleMonomorphism G.isRightSemimoduleMonomorphism
-    ; surjective                    = Func.surjective (_≈ᴹ_ M₁) _ _ (≈ᴹ-trans M₃) G.⟦⟧-cong F.surjective G.surjective
+    ; surjective                    = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective
     } where module F = IsRightSemimoduleIsomorphism f-iso; module G = IsRightSemimoduleIsomorphism g-iso
 
 module _
@@ -153,7 +153,7 @@ module _
                              IsRightModuleIsomorphism M₁ M₃ (g ∘ f)
   isRightModuleIsomorphism f-iso g-iso = record
     { isRightModuleMonomorphism = isRightModuleMonomorphism F.isRightModuleMonomorphism G.isRightModuleMonomorphism
-    ; surjective                = Func.surjective (_≈ᴹ_ M₁) _ _ (≈ᴹ-trans M₃) G.⟦⟧-cong F.surjective G.surjective
+    ; surjective                = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective
     } where module F = IsRightModuleIsomorphism f-iso; module G = IsRightModuleIsomorphism g-iso
 
 module _
@@ -189,7 +189,7 @@ module _
                               IsBisemimoduleIsomorphism M₁ M₃ (g ∘ f)
   isBisemimoduleIsomorphism f-iso g-iso = record
     { isBisemimoduleMonomorphism = isBisemimoduleMonomorphism F.isBisemimoduleMonomorphism G.isBisemimoduleMonomorphism
-    ; surjective                 = Func.surjective (_≈ᴹ_ M₁) _ _ (≈ᴹ-trans M₃) G.⟦⟧-cong F.surjective G.surjective
+    ; surjective                 = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective
     } where module F = IsBisemimoduleIsomorphism f-iso; module G = IsBisemimoduleIsomorphism g-iso
 
 module _
@@ -225,7 +225,7 @@ module _
                           IsBimoduleIsomorphism M₁ M₃ (g ∘ f)
   isBimoduleIsomorphism f-iso g-iso = record
     { isBimoduleMonomorphism = isBimoduleMonomorphism F.isBimoduleMonomorphism G.isBimoduleMonomorphism
-    ; surjective             = Func.surjective (_≈ᴹ_ M₁) _ _ (≈ᴹ-trans M₃) G.⟦⟧-cong F.surjective G.surjective
+    ; surjective             = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective
     } where module F = IsBimoduleIsomorphism f-iso; module G = IsBimoduleIsomorphism g-iso
 
 module _
@@ -258,7 +258,7 @@ module _
                             IsSemimoduleIsomorphism M₁ M₃ (g ∘ f)
   isSemimoduleIsomorphism f-iso g-iso = record
     { isSemimoduleMonomorphism = isSemimoduleMonomorphism F.isSemimoduleMonomorphism G.isSemimoduleMonomorphism
-    ; surjective               = Func.surjective (_≈ᴹ_ M₁) _ _ (≈ᴹ-trans M₃) G.⟦⟧-cong F.surjective G.surjective
+    ; surjective               = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective
     } where module F = IsSemimoduleIsomorphism f-iso; module G = IsSemimoduleIsomorphism g-iso
 
 module _
@@ -291,5 +291,5 @@ module _
                         IsModuleIsomorphism M₁ M₃ (g ∘ f)
   isModuleIsomorphism f-iso g-iso = record
     { isModuleMonomorphism = isModuleMonomorphism F.isModuleMonomorphism G.isModuleMonomorphism
-    ; surjective           = Func.surjective (_≈ᴹ_ M₁) _ _ (≈ᴹ-trans M₃) G.⟦⟧-cong F.surjective G.surjective
+    ; surjective           = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective
     } where module F = IsModuleIsomorphism f-iso; module G = IsModuleIsomorphism g-iso
diff --git a/src/Algebra/Module/Morphism/Construct/Identity.agda b/src/Algebra/Module/Morphism/Construct/Identity.agda
index 90f6940a16..55735c2b24 100644
--- a/src/Algebra/Module/Morphism/Construct/Identity.agda
+++ b/src/Algebra/Module/Morphism/Construct/Identity.agda
@@ -23,6 +23,7 @@ open import Algebra.Module.Morphism.Structures
 open import Algebra.Morphism.Construct.Identity
 open import Data.Product.Base using (_,_)
 open import Function.Base using (id)
+import Function.Construct.Identity as Id
 open import Level using (Level)
 
 private
@@ -48,7 +49,7 @@ module _ {semiring : Semiring r ℓr} (M : LeftSemimodule semiring m ℓm) where
   isLeftSemimoduleIsomorphism : IsLeftSemimoduleIsomorphism id
   isLeftSemimoduleIsomorphism = record
     { isLeftSemimoduleMonomorphism = isLeftSemimoduleMonomorphism
-    ; surjective                   = _, ≈ᴹ-refl
+    ; surjective                   = Id.surjective _
     }
 
 module _ {ring : Ring r ℓr} (M : LeftModule ring m ℓm) where
@@ -70,7 +71,7 @@ module _ {ring : Ring r ℓr} (M : LeftModule ring m ℓm) where
   isLeftModuleIsomorphism : IsLeftModuleIsomorphism id
   isLeftModuleIsomorphism = record
     { isLeftModuleMonomorphism = isLeftModuleMonomorphism
-    ; surjective               = _, ≈ᴹ-refl
+    ; surjective               = Id.surjective _
     }
 
 module _ {semiring : Semiring r ℓr} (M : RightSemimodule semiring m ℓm) where
@@ -92,7 +93,7 @@ module _ {semiring : Semiring r ℓr} (M : RightSemimodule semiring m ℓm) wher
   isRightSemimoduleIsomorphism : IsRightSemimoduleIsomorphism id
   isRightSemimoduleIsomorphism = record
     { isRightSemimoduleMonomorphism = isRightSemimoduleMonomorphism
-    ; surjective                    = _, ≈ᴹ-refl
+    ; surjective                    = Id.surjective _
     }
 
 module _ {ring : Ring r ℓr} (M : RightModule ring m ℓm) where
@@ -114,7 +115,7 @@ module _ {ring : Ring r ℓr} (M : RightModule ring m ℓm) where
   isRightModuleIsomorphism : IsRightModuleIsomorphism id
   isRightModuleIsomorphism = record
     { isRightModuleMonomorphism = isRightModuleMonomorphism
-    ; surjective                = _, ≈ᴹ-refl
+    ; surjective                = Id.surjective _
     }
 
 module _ {R-semiring : Semiring r ℓr} {S-semiring : Semiring s ℓs} (M : Bisemimodule R-semiring S-semiring m ℓm) where
@@ -137,7 +138,7 @@ module _ {R-semiring : Semiring r ℓr} {S-semiring : Semiring s ℓs} (M : Bise
   isBisemimoduleIsomorphism : IsBisemimoduleIsomorphism id
   isBisemimoduleIsomorphism = record
     { isBisemimoduleMonomorphism = isBisemimoduleMonomorphism
-    ; surjective                 = _, ≈ᴹ-refl
+    ; surjective                 = Id.surjective _
     }
 
 module _ {R-ring : Ring r ℓr} {S-ring : Ring r ℓr} (M : Bimodule R-ring S-ring m ℓm) where
@@ -160,7 +161,7 @@ module _ {R-ring : Ring r ℓr} {S-ring : Ring r ℓr} (M : Bimodule R-ring S-ri
   isBimoduleIsomorphism : IsBimoduleIsomorphism id
   isBimoduleIsomorphism = record
     { isBimoduleMonomorphism = isBimoduleMonomorphism
-    ; surjective             = _, ≈ᴹ-refl
+    ; surjective             = Id.surjective _
     }
 
 module _ {commutativeSemiring : CommutativeSemiring r ℓr} (M : Semimodule commutativeSemiring m ℓm) where
@@ -181,7 +182,7 @@ module _ {commutativeSemiring : CommutativeSemiring r ℓr} (M : Semimodule comm
   isSemimoduleIsomorphism : IsSemimoduleIsomorphism id
   isSemimoduleIsomorphism = record
     { isSemimoduleMonomorphism = isSemimoduleMonomorphism
-    ; surjective               = _, ≈ᴹ-refl
+    ; surjective               = Id.surjective _
     }
 
 module _ {commutativeRing : CommutativeRing r ℓr} (M : Module commutativeRing m ℓm) where
@@ -202,5 +203,5 @@ module _ {commutativeRing : CommutativeRing r ℓr} (M : Module commutativeRing
   isModuleIsomorphism : IsModuleIsomorphism id
   isModuleIsomorphism = record
     { isModuleMonomorphism = isModuleMonomorphism
-    ; surjective           = _, ≈ᴹ-refl
+    ; surjective           = Id.surjective _
     }
diff --git a/src/Algebra/Module/Morphism/Structures.agda b/src/Algebra/Module/Morphism/Structures.agda
index 3dc5fba3c5..96fb5ffa0a 100644
--- a/src/Algebra/Module/Morphism/Structures.agda
+++ b/src/Algebra/Module/Morphism/Structures.agda
@@ -11,7 +11,7 @@ open import Algebra.Bundles
 open import Algebra.Module.Bundles
 import Algebra.Module.Morphism.Definitions as MorphismDefinitions
 import Algebra.Morphism.Structures as MorphismStructures
-import Function.Definitions as FunctionDefinitions
+open import Function.Definitions
 open import Level
 
 private
@@ -28,7 +28,6 @@ module LeftSemimoduleMorphisms
   open LeftSemimodule M₁ renaming (Carrierᴹ to A; _*ₗ_ to _*ₗ₁_; _≈ᴹ_ to _≈ᴹ₁_)
   open LeftSemimodule M₂ renaming (Carrierᴹ to B; _*ₗ_ to _*ₗ₂_; _≈ᴹ_ to _≈ᴹ₂_)
   open MorphismDefinitions R A B _≈ᴹ₂_
-  open FunctionDefinitions _≈ᴹ₁_ _≈ᴹ₂_
   open MorphismStructures.MonoidMorphisms (LeftSemimodule.+ᴹ-rawMonoid M₁) (LeftSemimodule.+ᴹ-rawMonoid M₂)
 
   record IsLeftSemimoduleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where
@@ -43,7 +42,7 @@ module LeftSemimoduleMorphisms
   record IsLeftSemimoduleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
       isLeftSemimoduleHomomorphism : IsLeftSemimoduleHomomorphism ⟦_⟧
-      injective                    : Injective ⟦_⟧
+      injective                    : Injective  _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧
 
     open IsLeftSemimoduleHomomorphism isLeftSemimoduleHomomorphism public
 
@@ -60,7 +59,7 @@ module LeftSemimoduleMorphisms
   record IsLeftSemimoduleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
       isLeftSemimoduleMonomorphism : IsLeftSemimoduleMonomorphism ⟦_⟧
-      surjective                   : Surjective ⟦_⟧
+      surjective                   : Surjective  _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧
 
     open IsLeftSemimoduleMonomorphism isLeftSemimoduleMonomorphism public
 
@@ -84,7 +83,6 @@ module LeftModuleMorphisms
   open LeftModule M₁ renaming (Carrierᴹ to A; _*ₗ_ to _*ₗ₁_; _≈ᴹ_ to _≈ᴹ₁_)
   open LeftModule M₂ renaming (Carrierᴹ to B; _*ₗ_ to _*ₗ₂_; _≈ᴹ_ to _≈ᴹ₂_)
   open MorphismDefinitions R A B _≈ᴹ₂_
-  open FunctionDefinitions _≈ᴹ₁_ _≈ᴹ₂_
   open MorphismStructures.GroupMorphisms (LeftModule.+ᴹ-rawGroup M₁) (LeftModule.+ᴹ-rawGroup M₂)
   open LeftSemimoduleMorphisms (LeftModule.leftSemimodule M₁) (LeftModule.leftSemimodule M₂)
 
@@ -108,7 +106,7 @@ module LeftModuleMorphisms
   record IsLeftModuleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
       isLeftModuleHomomorphism : IsLeftModuleHomomorphism ⟦_⟧
-      injective                : Injective ⟦_⟧
+      injective                : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧
 
     open IsLeftModuleHomomorphism isLeftModuleHomomorphism public
 
@@ -130,7 +128,7 @@ module LeftModuleMorphisms
   record IsLeftModuleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
       isLeftModuleMonomorphism : IsLeftModuleMonomorphism ⟦_⟧
-      surjective               : Surjective ⟦_⟧
+      surjective               : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧
 
     open IsLeftModuleMonomorphism isLeftModuleMonomorphism public
 
@@ -159,7 +157,6 @@ module RightSemimoduleMorphisms
   open RightSemimodule M₁ renaming (Carrierᴹ to A; _*ᵣ_ to _*ᵣ₁_; _≈ᴹ_ to _≈ᴹ₁_)
   open RightSemimodule M₂ renaming (Carrierᴹ to B; _*ᵣ_ to _*ᵣ₂_; _≈ᴹ_ to _≈ᴹ₂_)
   open MorphismDefinitions R A B _≈ᴹ₂_
-  open FunctionDefinitions _≈ᴹ₁_ _≈ᴹ₂_
   open MorphismStructures.MonoidMorphisms (RightSemimodule.+ᴹ-rawMonoid M₁) (RightSemimodule.+ᴹ-rawMonoid M₂)
 
   record IsRightSemimoduleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where
@@ -174,7 +171,7 @@ module RightSemimoduleMorphisms
   record IsRightSemimoduleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
       isRightSemimoduleHomomorphism : IsRightSemimoduleHomomorphism ⟦_⟧
-      injective                    : Injective ⟦_⟧
+      injective                    : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧
 
     open IsRightSemimoduleHomomorphism isRightSemimoduleHomomorphism public
 
@@ -191,7 +188,7 @@ module RightSemimoduleMorphisms
   record IsRightSemimoduleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
       isRightSemimoduleMonomorphism : IsRightSemimoduleMonomorphism ⟦_⟧
-      surjective                   : Surjective ⟦_⟧
+      surjective                   : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧
 
     open IsRightSemimoduleMonomorphism isRightSemimoduleMonomorphism public
 
@@ -215,7 +212,6 @@ module RightModuleMorphisms
   open RightModule M₁ renaming (Carrierᴹ to A; _*ᵣ_ to _*ᵣ₁_; _≈ᴹ_ to _≈ᴹ₁_)
   open RightModule M₂ renaming (Carrierᴹ to B; _*ᵣ_ to _*ᵣ₂_; _≈ᴹ_ to _≈ᴹ₂_)
   open MorphismDefinitions R A B _≈ᴹ₂_
-  open FunctionDefinitions _≈ᴹ₁_ _≈ᴹ₂_
   open MorphismStructures.GroupMorphisms (RightModule.+ᴹ-rawGroup M₁) (RightModule.+ᴹ-rawGroup M₂)
   open RightSemimoduleMorphisms (RightModule.rightSemimodule M₁) (RightModule.rightSemimodule M₂)
 
@@ -238,7 +234,7 @@ module RightModuleMorphisms
   record IsRightModuleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
       isRightModuleHomomorphism : IsRightModuleHomomorphism ⟦_⟧
-      injective                : Injective ⟦_⟧
+      injective                : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧
 
     open IsRightModuleHomomorphism isRightModuleHomomorphism public
 
@@ -260,7 +256,7 @@ module RightModuleMorphisms
   record IsRightModuleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
       isRightModuleMonomorphism : IsRightModuleMonomorphism ⟦_⟧
-      surjective               : Surjective ⟦_⟧
+      surjective               : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧
 
     open IsRightModuleMonomorphism isRightModuleMonomorphism public
 
@@ -292,7 +288,6 @@ module BisemimoduleMorphisms
   open Bisemimodule M₂ renaming (Carrierᴹ to B; _*ₗ_ to _*ₗ₂_; _*ᵣ_ to _*ᵣ₂_; _≈ᴹ_ to _≈ᴹ₂_)
   open MorphismDefinitions R A B _≈ᴹ₂_ using (Homomorphicₗ)
   open MorphismDefinitions S A B _≈ᴹ₂_ using (Homomorphicᵣ)
-  open FunctionDefinitions _≈ᴹ₁_ _≈ᴹ₂_
   open MorphismStructures.MonoidMorphisms (Bisemimodule.+ᴹ-rawMonoid M₁) (Bisemimodule.+ᴹ-rawMonoid M₂)
   open LeftSemimoduleMorphisms (Bisemimodule.leftSemimodule M₁) (Bisemimodule.leftSemimodule M₂)
   open RightSemimoduleMorphisms (Bisemimodule.rightSemimodule M₁) (Bisemimodule.rightSemimodule M₂)
@@ -321,7 +316,7 @@ module BisemimoduleMorphisms
   record IsBisemimoduleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ s ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
       isBisemimoduleHomomorphism : IsBisemimoduleHomomorphism ⟦_⟧
-      injective                  : Injective ⟦_⟧
+      injective                  : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧
 
     open IsBisemimoduleHomomorphism isBisemimoduleHomomorphism public
 
@@ -343,7 +338,7 @@ module BisemimoduleMorphisms
   record IsBisemimoduleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ s ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
       isBisemimoduleMonomorphism : IsBisemimoduleMonomorphism ⟦_⟧
-      surjective                 : Surjective ⟦_⟧
+      surjective                 : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧
 
     open IsBisemimoduleMonomorphism isBisemimoduleMonomorphism public
 
@@ -375,7 +370,6 @@ module BimoduleMorphisms
   open Bimodule M₂ renaming (Carrierᴹ to B; _*ₗ_ to _*ₗ₂_; _*ᵣ_ to _*ᵣ₂_; _≈ᴹ_ to _≈ᴹ₂_)
   open MorphismDefinitions R A B _≈ᴹ₂_ using (Homomorphicₗ)
   open MorphismDefinitions S A B _≈ᴹ₂_ using (Homomorphicᵣ)
-  open FunctionDefinitions _≈ᴹ₁_ _≈ᴹ₂_
   open MorphismStructures.GroupMorphisms (Bimodule.+ᴹ-rawGroup M₁) (Bimodule.+ᴹ-rawGroup M₂)
   open LeftModuleMorphisms (Bimodule.leftModule M₁) (Bimodule.leftModule M₂)
   open RightModuleMorphisms (Bimodule.rightModule M₁) (Bimodule.rightModule M₂)
@@ -418,7 +412,7 @@ module BimoduleMorphisms
   record IsBimoduleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ s ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
       isBimoduleHomomorphism : IsBimoduleHomomorphism ⟦_⟧
-      injective              : Injective ⟦_⟧
+      injective              : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧
 
     open IsBimoduleHomomorphism isBimoduleHomomorphism public
 
@@ -459,7 +453,7 @@ module BimoduleMorphisms
   record IsBimoduleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ s ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
       isBimoduleMonomorphism : IsBimoduleMonomorphism ⟦_⟧
-      surjective             : Surjective ⟦_⟧
+      surjective             : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧
 
     open IsBimoduleMonomorphism isBimoduleMonomorphism public
 
@@ -505,7 +499,6 @@ module SemimoduleMorphisms
 
   open Semimodule M₁ renaming (Carrierᴹ to A; _≈ᴹ_ to _≈ᴹ₁_)
   open Semimodule M₂ renaming (Carrierᴹ to B; _≈ᴹ_ to _≈ᴹ₂_)
-  open FunctionDefinitions _≈ᴹ₁_ _≈ᴹ₂_
   open BisemimoduleMorphisms (Semimodule.bisemimodule M₁) (Semimodule.bisemimodule M₂)
 
   record IsSemimoduleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where
@@ -517,7 +510,7 @@ module SemimoduleMorphisms
   record IsSemimoduleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
       isSemimoduleHomomorphism : IsSemimoduleHomomorphism ⟦_⟧
-      injective                : Injective ⟦_⟧
+      injective                : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧
 
     open IsSemimoduleHomomorphism isSemimoduleHomomorphism public
 
@@ -535,7 +528,7 @@ module SemimoduleMorphisms
   record IsSemimoduleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
       isSemimoduleMonomorphism : IsSemimoduleMonomorphism ⟦_⟧
-      surjective               : Surjective ⟦_⟧
+      surjective               : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧
 
     open IsSemimoduleMonomorphism isSemimoduleMonomorphism public
 
@@ -558,7 +551,6 @@ module ModuleMorphisms
 
   open Module M₁ renaming (Carrierᴹ to A; _≈ᴹ_ to _≈ᴹ₁_)
   open Module M₂ renaming (Carrierᴹ to B; _≈ᴹ_ to _≈ᴹ₂_)
-  open FunctionDefinitions _≈ᴹ₁_ _≈ᴹ₂_
   open BimoduleMorphisms (Module.bimodule M₁) (Module.bimodule M₂)
   open SemimoduleMorphisms (Module.semimodule M₁) (Module.semimodule M₂)
 
@@ -576,7 +568,7 @@ module ModuleMorphisms
   record IsModuleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
       isModuleHomomorphism : IsModuleHomomorphism ⟦_⟧
-      injective            : Injective ⟦_⟧
+      injective            : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧
 
     open IsModuleHomomorphism isModuleHomomorphism public
 
@@ -601,7 +593,7 @@ module ModuleMorphisms
   record IsModuleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
       isModuleMonomorphism : IsModuleMonomorphism ⟦_⟧
-      surjective           : Surjective ⟦_⟧
+      surjective           : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧
 
     open IsModuleMonomorphism isModuleMonomorphism public
 
diff --git a/src/Algebra/Morphism/Consequences.agda b/src/Algebra/Morphism/Consequences.agda
index c81e55a7bb..96175740e6 100644
--- a/src/Algebra/Morphism/Consequences.agda
+++ b/src/Algebra/Morphism/Consequences.agda
@@ -29,10 +29,10 @@ module _ {α α= β β=} (M₁ : Magma α α=) (M₂ : Magma β β=) where
                       Inverseᵇ _≈₁_ _≈₂_ f g →
                       Homomorphic₂ _ _ _≈₂_ f _∙₁_ _∙₂_  →
                       Homomorphic₂ _ _ _≈₁_ g _∙₂_ _∙₁_
-  homomorphic₂-inv {f} {g} g-cong (f∘g=id , g∘f=id) homo x y = begin
-    g (x ∙₂ y)             ≈⟨ M₁.sym (g-cong (M₂.∙-cong (f∘g=id x) (f∘g=id y))) ⟩
-    g (f (g x) ∙₂ f (g y)) ≈⟨ M₁.sym (g-cong (homo (g x) (g y))) ⟩
-    g (f (g x ∙₁ g y))     ≈⟨ g∘f=id (g x ∙₁ g y) ⟩
+  homomorphic₂-inv {f} {g} g-cong (invˡ , invʳ) homo x y = begin
+    g (x ∙₂ y)             ≈˘⟨ g-cong (M₂.∙-cong (invˡ M₁.refl) (invˡ M₁.refl)) ⟩
+    g (f (g x) ∙₂ f (g y)) ≈˘⟨ g-cong (homo (g x) (g y)) ⟩
+    g (f (g x ∙₁ g y))     ≈⟨ invʳ M₂.refl ⟩
     g x ∙₁ g y             ∎
     where open EqR M₁.setoid
 
@@ -41,8 +41,8 @@ module _ {α α= β β=} (M₁ : Magma α α=) (M₂ : Magma β β=) where
                       Homomorphic₂ _ _ _≈₂_ f _∙₁_ _∙₂_  →
                       Homomorphic₂ _ _ _≈₁_ g _∙₂_ _∙₁_
   homomorphic₂-inj {f} {g} inj invˡ homo x y = inj (begin
-    f (g (x ∙₂ y))      ≈⟨ invˡ (x ∙₂ y) ⟩
-    x ∙₂ y              ≈⟨ M₂.sym (M₂.∙-cong (invˡ x) (invˡ y)) ⟩
-    f (g x) ∙₂ f (g y)  ≈⟨ M₂.sym (homo (g x) (g y)) ⟩
+    f (g (x ∙₂ y))      ≈⟨ invˡ M₁.refl ⟩
+    x ∙₂ y              ≈˘⟨ M₂.∙-cong (invˡ M₁.refl) (invˡ M₁.refl) ⟩
+    f (g x) ∙₂ f (g y)  ≈˘⟨ homo (g x) (g y) ⟩
     f (g x ∙₁ g y)      ∎)
     where open EqR M₂.setoid
diff --git a/src/Algebra/Morphism/Construct/Composition.agda b/src/Algebra/Morphism/Construct/Composition.agda
index 991fb93433..e3f3a3ad71 100644
--- a/src/Algebra/Morphism/Construct/Composition.agda
+++ b/src/Algebra/Morphism/Construct/Composition.agda
@@ -57,7 +57,7 @@ module _ {M₁ : RawMagma a ℓ₁}
     → IsMagmaIsomorphism M₁ M₃ (g ∘ f)
   isMagmaIsomorphism f-iso g-iso = record
     { isMagmaMonomorphism = isMagmaMonomorphism F.isMagmaMonomorphism G.isMagmaMonomorphism
-    ; surjective          = Func.surjective (_≈_ M₁) _ _ ≈₃-trans G.⟦⟧-cong F.surjective G.surjective
+    ; surjective          = Func.surjective _ _ (_≈_ M₃) F.surjective G.surjective
     } where module F = IsMagmaIsomorphism f-iso; module G = IsMagmaIsomorphism g-iso
 
 
@@ -97,7 +97,7 @@ module _ {M₁ : RawMonoid a ℓ₁}
     → IsMonoidIsomorphism M₁ M₃ (g ∘ f)
   isMonoidIsomorphism f-iso g-iso = record
     { isMonoidMonomorphism = isMonoidMonomorphism F.isMonoidMonomorphism G.isMonoidMonomorphism
-    ; surjective           = Func.surjective (_≈_ M₁) _ _ ≈₃-trans G.⟦⟧-cong F.surjective G.surjective
+    ; surjective           = Func.surjective _ _(_≈_ M₃)  F.surjective G.surjective
     } where module F = IsMonoidIsomorphism f-iso; module G = IsMonoidIsomorphism g-iso
 
 
@@ -138,7 +138,7 @@ module _ {G₁ : RawGroup a ℓ₁}
     → IsGroupIsomorphism G₁ G₃ (g ∘ f)
   isGroupIsomorphism f-iso g-iso = record
     { isGroupMonomorphism = isGroupMonomorphism F.isGroupMonomorphism G.isGroupMonomorphism
-    ; surjective          = Func.surjective (_≈_ G₁) _ _ ≈₃-trans G.⟦⟧-cong F.surjective G.surjective
+    ; surjective          = Func.surjective  _ _ (_≈_ G₃) F.surjective G.surjective
     } where module F = IsGroupIsomorphism f-iso; module G = IsGroupIsomorphism g-iso
 
 
@@ -178,7 +178,7 @@ module _ {R₁ : RawNearSemiring a ℓ₁}
     → IsNearSemiringIsomorphism R₁ R₃ (g ∘ f)
   isNearSemiringIsomorphism f-iso g-iso = record
     { isNearSemiringMonomorphism = isNearSemiringMonomorphism F.isNearSemiringMonomorphism G.isNearSemiringMonomorphism
-    ; surjective                 = Func.surjective (_≈_ R₁) _ _ ≈₃-trans G.⟦⟧-cong F.surjective G.surjective
+    ; surjective                 = Func.surjective _ _ (_≈_ R₃) F.surjective G.surjective
     } where module F = IsNearSemiringIsomorphism f-iso; module G = IsNearSemiringIsomorphism g-iso
 
 
@@ -220,7 +220,7 @@ module _
     → IsSemiringIsomorphism R₁ R₃ (g ∘ f)
   isSemiringIsomorphism f-iso g-iso = record
     { isSemiringMonomorphism = isSemiringMonomorphism F.isSemiringMonomorphism G.isSemiringMonomorphism
-    ; surjective             = Func.surjective (_≈_ R₁) _ _ ≈₃-trans G.⟦⟧-cong F.surjective G.surjective
+    ; surjective             = Func.surjective _ _ (_≈_ R₃) F.surjective G.surjective
     } where module F = IsSemiringIsomorphism f-iso; module G = IsSemiringIsomorphism g-iso
 
 ------------------------------------------------------------------------
@@ -260,7 +260,7 @@ module _ {R₁ : RawRingWithoutOne a ℓ₁}
     → IsRingWithoutOneIsoMorphism R₁ R₃ (g ∘ f)
   isRingWithoutOneIsoMorphism f-iso g-iso = record
     { isRingWithoutOneMonomorphism = isRingWithoutOneMonomorphism F.isRingWithoutOneMonomorphism G.isRingWithoutOneMonomorphism
-    ; surjective         = Func.surjective (_≈_ R₁) (_≈_ R₂) (_≈_ R₃) ≈₃-trans G.⟦⟧-cong F.surjective G.surjective
+    ; surjective         = Func.surjective _ _ (_≈_ R₃) F.surjective G.surjective
     } where module F = IsRingWithoutOneIsoMorphism f-iso; module G = IsRingWithoutOneIsoMorphism g-iso
 
 ------------------------------------------------------------------------
@@ -300,7 +300,7 @@ module _ {R₁ : RawRing a ℓ₁}
     → IsRingIsomorphism R₁ R₃ (g ∘ f)
   isRingIsomorphism f-iso g-iso = record
     { isRingMonomorphism = isRingMonomorphism F.isRingMonomorphism G.isRingMonomorphism
-    ; surjective         = Func.surjective (_≈_ R₁) _ _ ≈₃-trans G.⟦⟧-cong F.surjective G.surjective
+    ; surjective         = Func.surjective _ _ (_≈_ R₃) F.surjective G.surjective
     } where module F = IsRingIsomorphism f-iso; module G = IsRingIsomorphism g-iso
 
 ------------------------------------------------------------------------
@@ -342,7 +342,7 @@ module _ {Q₁ : RawQuasigroup a ℓ₁}
     → IsQuasigroupIsomorphism Q₁ Q₃ (g ∘ f)
   isQuasigroupIsomorphism f-iso g-iso = record
     { isQuasigroupMonomorphism = isQuasigroupMonomorphism F.isQuasigroupMonomorphism G.isQuasigroupMonomorphism
-    ; surjective               = Func.surjective (_≈_ Q₁) (_≈_ Q₂) (_≈_ Q₃) ≈₃-trans G.⟦⟧-cong F.surjective G.surjective
+    ; surjective               = Func.surjective _ _ (_≈_ Q₃) F.surjective G.surjective
     } where module F = IsQuasigroupIsomorphism f-iso; module G = IsQuasigroupIsomorphism g-iso
 
 ------------------------------------------------------------------------
@@ -382,5 +382,5 @@ module _ {L₁ : RawLoop a ℓ₁}
     → IsLoopIsomorphism L₁ L₃ (g ∘ f)
   isLoopIsomorphism f-iso g-iso = record
     { isLoopMonomorphism = isLoopMonomorphism F.isLoopMonomorphism G.isLoopMonomorphism
-    ; surjective               = Func.surjective (_≈_ L₁) (_≈_ L₂) (_≈_ L₃) ≈₃-trans G.⟦⟧-cong F.surjective G.surjective
+    ; surjective         = Func.surjective _ _ (_≈_ L₃) F.surjective G.surjective
     } where module F = IsLoopIsomorphism f-iso; module G = IsLoopIsomorphism g-iso
diff --git a/src/Algebra/Morphism/Construct/Identity.agda b/src/Algebra/Morphism/Construct/Identity.agda
index 5529ec3c01..63e95e54e6 100644
--- a/src/Algebra/Morphism/Construct/Identity.agda
+++ b/src/Algebra/Morphism/Construct/Identity.agda
@@ -22,6 +22,7 @@ open import Algebra.Morphism.Structures
         )
 open import Data.Product.Base using (_,_)
 open import Function.Base using (id)
+import Function.Construct.Identity as Id
 open import Level using (Level)
 open import Relation.Binary.Morphism.Construct.Identity using (isRelHomomorphism)
 open import Relation.Binary.Definitions using (Reflexive)
@@ -51,7 +52,7 @@ module _ (M : RawMagma c ℓ) (open RawMagma M) (refl : Reflexive _≈_) where
   isMagmaIsomorphism : IsMagmaIsomorphism id
   isMagmaIsomorphism = record
     { isMagmaMonomorphism = isMagmaMonomorphism
-    ; surjective = _, refl
+    ; surjective = Id.surjective _
     }
 
 ------------------------------------------------------------------------
@@ -75,7 +76,7 @@ module _ (M : RawMonoid c ℓ) (open RawMonoid M) (refl : Reflexive _≈_) where
   isMonoidIsomorphism : IsMonoidIsomorphism id
   isMonoidIsomorphism = record
     { isMonoidMonomorphism = isMonoidMonomorphism
-    ; surjective = _, refl
+    ; surjective = Id.surjective _
     }
 
 ------------------------------------------------------------------------
@@ -99,7 +100,7 @@ module _ (G : RawGroup c ℓ) (open RawGroup G) (refl : Reflexive _≈_) where
   isGroupIsomorphism : IsGroupIsomorphism id
   isGroupIsomorphism = record
     { isGroupMonomorphism = isGroupMonomorphism
-    ; surjective = _, refl
+    ; surjective = Id.surjective _
     }
 
 ------------------------------------------------------------------------
@@ -123,7 +124,7 @@ module _ (R : RawNearSemiring c ℓ) (open RawNearSemiring R) (refl : Reflexive
   isNearSemiringIsomorphism : IsNearSemiringIsomorphism id
   isNearSemiringIsomorphism = record
     { isNearSemiringMonomorphism = isNearSemiringMonomorphism
-    ; surjective = _, refl
+    ; surjective = Id.surjective _
     }
 
 ------------------------------------------------------------------------
@@ -147,7 +148,7 @@ module _ (R : RawSemiring c ℓ) (open RawSemiring R) (refl : Reflexive _≈_) w
   isSemiringIsomorphism : IsSemiringIsomorphism id
   isSemiringIsomorphism = record
     { isSemiringMonomorphism = isSemiringMonomorphism
-    ; surjective = _, refl
+    ; surjective = Id.surjective _
     }
 
 ------------------------------------------------------------------------
@@ -171,7 +172,7 @@ module _ (R : RawRingWithoutOne c ℓ) (open RawRingWithoutOne R) (refl : Reflex
   isRingWithoutOneIsoMorphism : IsRingWithoutOneIsoMorphism id
   isRingWithoutOneIsoMorphism = record
     { isRingWithoutOneMonomorphism = isRingWithoutOneMonomorphism
-    ; surjective = _, refl
+    ; surjective = Id.surjective _
     }
 
 ------------------------------------------------------------------------
@@ -195,7 +196,7 @@ module _ (R : RawRing c ℓ) (open RawRing R) (refl : Reflexive _≈_) where
   isRingIsomorphism : IsRingIsomorphism id
   isRingIsomorphism = record
     { isRingMonomorphism = isRingMonomorphism
-    ; surjective = _, refl
+    ; surjective = Id.surjective _
     }
 
 ------------------------------------------------------------------------
@@ -221,7 +222,7 @@ module _ (Q : RawQuasigroup c ℓ) (open RawQuasigroup Q) (refl : Reflexive _≈
   isQuasigroupIsomorphism : IsQuasigroupIsomorphism id
   isQuasigroupIsomorphism = record
     { isQuasigroupMonomorphism = isQuasigroupMonomorphism
-    ; surjective = _, refl
+    ; surjective = Id.surjective _
     }
 
 ------------------------------------------------------------------------
@@ -245,5 +246,5 @@ module _ (L : RawLoop c ℓ) (open RawLoop L) (refl : Reflexive _≈_) where
   isLoopIsomorphism : IsLoopIsomorphism id
   isLoopIsomorphism = record
     { isLoopMonomorphism = isLoopMonomorphism
-    ; surjective = _, refl
+    ; surjective = Id.surjective _
     }
diff --git a/src/Algebra/Morphism/Structures.agda b/src/Algebra/Morphism/Structures.agda
index 525cbf5da0..eb8970ba5c 100644
--- a/src/Algebra/Morphism/Structures.agda
+++ b/src/Algebra/Morphism/Structures.agda
@@ -14,7 +14,7 @@ open import Algebra.Core
 open import Algebra.Bundles
 import Algebra.Morphism.Definitions as MorphismDefinitions
 open import Level using (Level; _⊔_)
-import Function.Definitions as FunctionDefinitions
+open import Function.Definitions
 open import Relation.Binary.Morphism.Structures
 
 private
@@ -30,7 +30,6 @@ module MagmaMorphisms (M₁ : RawMagma a ℓ₁) (M₂ : RawMagma b ℓ₂) wher
   open RawMagma M₁ renaming (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_)
   open RawMagma M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_)
   open MorphismDefinitions A B _≈₂_
-  open FunctionDefinitions _≈₁_ _≈₂_
 
 
   record IsMagmaHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
@@ -45,7 +44,7 @@ module MagmaMorphisms (M₁ : RawMagma a ℓ₁) (M₂ : RawMagma b ℓ₂) wher
   record IsMagmaMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isMagmaHomomorphism : IsMagmaHomomorphism ⟦_⟧
-      injective           : Injective ⟦_⟧
+      injective           : Injective _≈₁_ _≈₂_ ⟦_⟧
 
     open IsMagmaHomomorphism isMagmaHomomorphism public
 
@@ -59,7 +58,7 @@ module MagmaMorphisms (M₁ : RawMagma a ℓ₁) (M₂ : RawMagma b ℓ₂) wher
   record IsMagmaIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isMagmaMonomorphism : IsMagmaMonomorphism ⟦_⟧
-      surjective          : Surjective ⟦_⟧
+      surjective          : Surjective _≈₁_ _≈₂_ ⟦_⟧
 
     open IsMagmaMonomorphism isMagmaMonomorphism public
 
@@ -79,7 +78,6 @@ module MonoidMorphisms (M₁ : RawMonoid a ℓ₁) (M₂ : RawMonoid b ℓ₂) w
   open RawMonoid M₁ renaming (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_; ε to ε₁)
   open RawMonoid M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; ε to ε₂)
   open MorphismDefinitions A B _≈₂_
-  open FunctionDefinitions _≈₁_ _≈₂_
   open MagmaMorphisms (RawMonoid.rawMagma M₁) (RawMonoid.rawMagma M₂)
 
 
@@ -94,7 +92,7 @@ module MonoidMorphisms (M₁ : RawMonoid a ℓ₁) (M₂ : RawMonoid b ℓ₂) w
   record IsMonoidMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isMonoidHomomorphism : IsMonoidHomomorphism ⟦_⟧
-      injective            : Injective ⟦_⟧
+      injective            : Injective _≈₁_ _≈₂_ ⟦_⟧
 
     open IsMonoidHomomorphism isMonoidHomomorphism public
 
@@ -111,7 +109,7 @@ module MonoidMorphisms (M₁ : RawMonoid a ℓ₁) (M₂ : RawMonoid b ℓ₂) w
   record IsMonoidIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isMonoidMonomorphism : IsMonoidMonomorphism ⟦_⟧
-      surjective           : Surjective ⟦_⟧
+      surjective           : Surjective _≈₁_ _≈₂_ ⟦_⟧
 
     open IsMonoidMonomorphism isMonoidMonomorphism public
 
@@ -136,7 +134,6 @@ module GroupMorphisms (G₁ : RawGroup a ℓ₁) (G₂ : RawGroup b ℓ₂) wher
   open RawGroup G₂ renaming
     (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; _⁻¹ to _⁻¹₂; ε to ε₂)
   open MorphismDefinitions A B _≈₂_
-  open FunctionDefinitions _≈₁_ _≈₂_
   open MagmaMorphisms  (RawGroup.rawMagma  G₁) (RawGroup.rawMagma  G₂)
   open MonoidMorphisms (RawGroup.rawMonoid G₁) (RawGroup.rawMonoid G₂)
 
@@ -152,7 +149,7 @@ module GroupMorphisms (G₁ : RawGroup a ℓ₁) (G₂ : RawGroup b ℓ₂) wher
   record IsGroupMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isGroupHomomorphism : IsGroupHomomorphism ⟦_⟧
-      injective           : Injective ⟦_⟧
+      injective           : Injective _≈₁_ _≈₂_ ⟦_⟧
 
     open IsGroupHomomorphism isGroupHomomorphism public
       renaming (homo to ∙-homo)
@@ -170,7 +167,7 @@ module GroupMorphisms (G₁ : RawGroup a ℓ₁) (G₂ : RawGroup b ℓ₂) wher
   record IsGroupIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isGroupMonomorphism : IsGroupMonomorphism ⟦_⟧
-      surjective          : Surjective ⟦_⟧
+      surjective          : Surjective _≈₁_ _≈₂_ ⟦_⟧
 
     open IsGroupMonomorphism isGroupMonomorphism public
 
@@ -207,7 +204,6 @@ module NearSemiringMorphisms (R₁ : RawNearSemiring a ℓ₁) (R₂ : RawNearSe
     module * = MagmaMorphisms *-rawMagma₁ *-rawMagma₂
 
   open MorphismDefinitions A B _≈₂_
-  open FunctionDefinitions _≈₁_ _≈₂_
 
 
   record IsNearSemiringHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
@@ -227,7 +223,7 @@ module NearSemiringMorphisms (R₁ : RawNearSemiring a ℓ₁) (R₂ : RawNearSe
   record IsNearSemiringMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isNearSemiringHomomorphism : IsNearSemiringHomomorphism ⟦_⟧
-      injective          : Injective ⟦_⟧
+      injective          : Injective _≈₁_ _≈₂_ ⟦_⟧
 
     open IsNearSemiringHomomorphism isNearSemiringHomomorphism public
 
@@ -250,7 +246,7 @@ module NearSemiringMorphisms (R₁ : RawNearSemiring a ℓ₁) (R₂ : RawNearSe
   record IsNearSemiringIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isNearSemiringMonomorphism : IsNearSemiringMonomorphism ⟦_⟧
-      surjective                 : Surjective ⟦_⟧
+      surjective                 : Surjective _≈₁_ _≈₂_ ⟦_⟧
 
     open IsNearSemiringMonomorphism isNearSemiringMonomorphism public
 
@@ -292,7 +288,6 @@ module SemiringMorphisms (R₁ : RawSemiring a ℓ₁) (R₂ : RawSemiring b ℓ
     module * = MonoidMorphisms *-rawMonoid₁ *-rawMonoid₂
 
   open MorphismDefinitions A B _≈₂_
-  open FunctionDefinitions _≈₁_ _≈₂_
   open NearSemiringMorphisms rawNearSemiring₁ rawNearSemiring₂
 
   record IsSemiringHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
@@ -311,7 +306,7 @@ module SemiringMorphisms (R₁ : RawSemiring a ℓ₁) (R₂ : RawSemiring b ℓ
   record IsSemiringMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isSemiringHomomorphism : IsSemiringHomomorphism ⟦_⟧
-      injective              : Injective ⟦_⟧
+      injective              : Injective _≈₁_ _≈₂_ ⟦_⟧
 
     open IsSemiringHomomorphism isSemiringHomomorphism public
 
@@ -333,7 +328,7 @@ module SemiringMorphisms (R₁ : RawSemiring a ℓ₁) (R₂ : RawSemiring b ℓ
   record IsSemiringIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isSemiringMonomorphism : IsSemiringMonomorphism ⟦_⟧
-      surjective             : Surjective ⟦_⟧
+      surjective             : Surjective _≈₁_ _≈₂_ ⟦_⟧
 
     open IsSemiringMonomorphism isSemiringMonomorphism public
 
@@ -375,7 +370,6 @@ module RingWithoutOneMorphisms (R₁ : RawRingWithoutOne a ℓ₁) (R₂ : RawRi
     module * = MagmaMorphisms *-rawMagma₁ *-rawMagma₂
 
   open MorphismDefinitions A B _≈₂_
-  open FunctionDefinitions _≈₁_ _≈₂_
 
   record IsRingWithoutOneHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
     field
@@ -394,7 +388,7 @@ module RingWithoutOneMorphisms (R₁ : RawRingWithoutOne a ℓ₁) (R₂ : RawRi
   record IsRingWithoutOneMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isRingWithoutOneHomomorphism : IsRingWithoutOneHomomorphism ⟦_⟧
-      injective                    : Injective ⟦_⟧
+      injective                    : Injective _≈₁_ _≈₂_ ⟦_⟧
 
     open IsRingWithoutOneHomomorphism isRingWithoutOneHomomorphism public
 
@@ -417,7 +411,7 @@ module RingWithoutOneMorphisms (R₁ : RawRingWithoutOne a ℓ₁) (R₂ : RawRi
   record IsRingWithoutOneIsoMorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isRingWithoutOneMonomorphism : IsRingWithoutOneMonomorphism ⟦_⟧
-      surjective                   : Surjective ⟦_⟧
+      surjective                   : Surjective _≈₁_ _≈₂_ ⟦_⟧
 
     open IsRingWithoutOneMonomorphism isRingWithoutOneMonomorphism public
 
@@ -462,7 +456,6 @@ module RingMorphisms (R₁ : RawRing a ℓ₁) (R₂ : RawRing b ℓ₂) where
   module * = MonoidMorphisms *-rawMonoid₁ *-rawMonoid₂
 
   open MorphismDefinitions A B _≈₂_
-  open FunctionDefinitions _≈₁_ _≈₂_
   open SemiringMorphisms rawSemiring₁ rawSemiring₂
 
 
@@ -482,7 +475,7 @@ module RingMorphisms (R₁ : RawRing a ℓ₁) (R₂ : RawRing b ℓ₂) where
   record IsRingMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isRingHomomorphism : IsRingHomomorphism ⟦_⟧
-      injective          : Injective ⟦_⟧
+      injective          : Injective _≈₁_ _≈₂_ ⟦_⟧
 
     open IsRingHomomorphism isRingHomomorphism public
 
@@ -518,7 +511,7 @@ module RingMorphisms (R₁ : RawRing a ℓ₁) (R₂ : RawRing b ℓ₂) where
   record IsRingIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isRingMonomorphism : IsRingMonomorphism ⟦_⟧
-      surjective         : Surjective ⟦_⟧
+      surjective         : Surjective _≈₁_ _≈₂_ ⟦_⟧
 
     open IsRingMonomorphism isRingMonomorphism public
 
@@ -568,7 +561,6 @@ module QuasigroupMorphisms (Q₁ : RawQuasigroup a ℓ₁) (Q₂ : RawQuasigroup
   module // = MagmaMorphisms //-rawMagma₁ //-rawMagma₂
 
   open MorphismDefinitions A B _≈₂_
-  open FunctionDefinitions _≈₁_ _≈₂_
 
   record IsQuasigroupHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
     field
@@ -601,7 +593,7 @@ module QuasigroupMorphisms (Q₁ : RawQuasigroup a ℓ₁) (Q₂ : RawQuasigroup
   record IsQuasigroupMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isQuasigroupHomomorphism : IsQuasigroupHomomorphism ⟦_⟧
-      injective                : Injective ⟦_⟧
+      injective                : Injective _≈₁_ _≈₂_ ⟦_⟧
 
     open IsQuasigroupHomomorphism isQuasigroupHomomorphism public
 
@@ -631,7 +623,7 @@ module QuasigroupMorphisms (Q₁ : RawQuasigroup a ℓ₁) (Q₂ : RawQuasigroup
   record IsQuasigroupIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isQuasigroupMonomorphism : IsQuasigroupMonomorphism ⟦_⟧
-      surjective               : Surjective ⟦_⟧
+      surjective               : Surjective _≈₁_ _≈₂_ ⟦_⟧
 
     open IsQuasigroupMonomorphism isQuasigroupMonomorphism public
 
@@ -669,7 +661,6 @@ module LoopMorphisms (L₁ : RawLoop a ℓ₁) (L₂ : RawLoop b ℓ₂) where
                             \\-rawMagma to \\-rawMagma₂; //-rawMagma to //-rawMagma₂;
                             _≈_ to _≈₂_; _∙_ to _∙₂_; _\\_ to _\\₂_; _//_ to _//₂_ ; ε to ε₂)
   open MorphismDefinitions A B _≈₂_
-  open FunctionDefinitions _≈₁_ _≈₂_
 
   open QuasigroupMorphisms (RawLoop.rawQuasigroup L₁) (RawLoop.rawQuasigroup L₂)
 
@@ -683,14 +674,14 @@ module LoopMorphisms (L₁ : RawLoop a ℓ₁) (L₂ : RawLoop b ℓ₂) where
   record IsLoopMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isLoopHomomorphism   : IsLoopHomomorphism ⟦_⟧
-      injective            : Injective ⟦_⟧
+      injective            : Injective _≈₁_ _≈₂_ ⟦_⟧
 
     open IsLoopHomomorphism isLoopHomomorphism public
 
   record IsLoopIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isLoopMonomorphism   : IsLoopMonomorphism ⟦_⟧
-      surjective           : Surjective ⟦_⟧
+      surjective           : Surjective _≈₁_ _≈₂_ ⟦_⟧
 
     open IsLoopMonomorphism isLoopMonomorphism public
 
diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index 9c7cbdf170..5fe0fa0b2c 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 (Inverseˡ; Inverseʳ)
+open import Function.Definitions
 open import Function.Equality using (_⟨$⟩_)
 open import Function.Properties.Inverse using (↔⇒↣)
 open import Function.Base using (_∘_)
@@ -57,7 +57,7 @@ Permutation′ n = Permutation n n
 -- Helper functions
 
 permutation : ∀ (f : Fin m → Fin n) (g : Fin n → Fin m) →
-              Inverseˡ _≡_ _≡_ f g → Inverseʳ _≡_ _≡_ f g → Permutation m n
+              StrictlyInverseˡ _≡_ f g → StrictlyInverseʳ _≡_ f g → Permutation m n
 permutation = mk↔′
 
 infixl 5 _⟨$⟩ʳ_ _⟨$⟩ˡ_
@@ -68,10 +68,10 @@ _⟨$⟩ˡ_ : Permutation m n → Fin n → Fin m
 _⟨$⟩ˡ_ = Inverse.from
 
 inverseˡ : ∀ (π : Permutation m n) {i} → π ⟨$⟩ˡ (π ⟨$⟩ʳ i) ≡ i
-inverseˡ π = Inverse.inverseʳ π _
+inverseˡ π = Inverse.inverseʳ π P.refl
 
 inverseʳ : ∀ (π : Permutation m n) {i} → π ⟨$⟩ʳ (π ⟨$⟩ˡ i) ≡ i
-inverseʳ π = Inverse.inverseˡ π _
+inverseʳ π = Inverse.inverseˡ π P.refl
 
 ------------------------------------------------------------------------
 -- Equality
@@ -142,7 +142,7 @@ remove {m} {n} i π = permutation to from inverseˡ′ inverseʳ′
   from : Fin n → Fin m
   from j = punchOut {j = πˡ (punchIn (πʳ i) j)} from-punchOut
 
-  inverseʳ′ : Inverseʳ _≡_ _≡_ to from
+  inverseʳ′ : StrictlyInverseʳ _≡_ to from
   inverseʳ′ j = begin
     from (to j)                                                      ≡⟨⟩
     punchOut {i = i} {πˡ (punchIn (πʳ i) (punchOut to-punchOut))} _  ≡⟨ punchOut-cong′ i (cong πˡ (punchIn-punchOut _)) ⟩
@@ -150,7 +150,7 @@ remove {m} {n} i π = permutation to from inverseˡ′ inverseʳ′
     punchOut {i = i} {punchIn i j}                                _  ≡⟨ punchOut-punchIn i ⟩
     j                                                                ∎
 
-  inverseˡ′ : Inverseˡ _≡_ _≡_ to from
+  inverseˡ′ : StrictlyInverseˡ _≡_ to from
   inverseˡ′ j = begin
     to (from j)                                                       ≡⟨⟩
     punchOut {i = πʳ i} {πʳ (punchIn i (punchOut from-punchOut))}  _  ≡⟨ punchOut-cong′ (πʳ i) (cong πʳ (punchIn-punchOut _)) ⟩
@@ -171,11 +171,11 @@ lift₀ {m} {n} π = permutation to from inverseˡ′ inverseʳ′
   from 0F      = 0F
   from (suc i) = suc (π ⟨$⟩ˡ i)
 
-  inverseʳ′ : Inverseʳ _≡_ _≡_ to from
+  inverseʳ′ : StrictlyInverseʳ _≡_ to from
   inverseʳ′ 0F      = refl
   inverseʳ′ (suc j) = cong suc (inverseˡ π)
 
-  inverseˡ′ : Inverseˡ _≡_ _≡_ to from
+  inverseˡ′ : StrictlyInverseˡ _≡_ to from
   inverseˡ′ 0F      = refl
   inverseˡ′ (suc j) = cong suc (inverseʳ π)
 
@@ -194,7 +194,7 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
   ... | yes j≡k = i
   ... | no  j≢k = punchIn i (π ⟨$⟩ˡ punchOut j≢k)
 
-  inverseʳ′ : Inverseʳ _≡_ _≡_ to from
+  inverseʳ′ : StrictlyInverseʳ _≡_ to from
   inverseʳ′ k with i ≟ k
   ... | yes i≡k rewrite proj₂ (dec-yes (j ≟ j) refl) = i≡k
   ... | no  i≢k
@@ -207,7 +207,7 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
     punchIn i (punchOut i≢k)                                              ≡⟨ punchIn-punchOut i≢k ⟩
     k                                                                     ∎
 
-  inverseˡ′ : Inverseˡ _≡_ _≡_ to from
+  inverseˡ′ : StrictlyInverseˡ _≡_ to from
   inverseˡ′ k with j ≟ k
   ... | yes j≡k rewrite proj₂ (dec-yes (i ≟ i) refl) = j≡k
   ... | no  j≢k
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 615728e971..2bacfe58ca 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -31,9 +31,8 @@ open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′)
 open import Data.Sum.Properties using ([,]-map; [,]-∘)
 open import Function.Base using (_∘_; id; _$_; flip)
 open import Function.Bundles using (Injection; _↣_; _⇔_; _↔_; mk⇔; mk↔′)
-open import Function.Definitions using (Injective)
-open import Function.Definitions.Core2 using (Surjective)
-open import Function.Consequences using (contraInjective)
+open import Function.Definitions using (Injective; Surjective)
+open import Function.Consequences.Propositional using (contraInjective)
 open import Function.Construct.Composition as Comp hiding (injective)
 open import Level using (Level)
 open import Relation.Binary as B hiding (Decidable; _⇔_)
@@ -870,10 +869,10 @@ punchOut-punchIn (suc i) {suc j} = cong suc (begin
 -- pinch
 ------------------------------------------------------------------------
 
-pinch-surjective : ∀ (i : Fin n) → Surjective _≡_ (pinch i)
-pinch-surjective _       zero    = zero , refl
-pinch-surjective zero    (suc j) = suc (suc j) , refl
-pinch-surjective (suc i) (suc j) = map suc (cong suc) (pinch-surjective i j)
+pinch-surjective : ∀ (i : Fin n) → Surjective _≡_ _≡_ (pinch i)
+pinch-surjective _       zero    = zero , λ { refl → refl }
+pinch-surjective zero    (suc j) = suc (suc j) , λ { refl → refl }
+pinch-surjective (suc i) (suc j) = map suc (λ {f refl → cong suc (f refl)}) (pinch-surjective i j)
 
 pinch-mono-≤ : ∀ (i : Fin n) → (pinch i) Preserves _≤_ ⟶ _≤_
 pinch-mono-≤ 0F      {0F}    {k}     0≤n       = z≤n
@@ -990,8 +989,8 @@ injective⇒≤ {zero}  {_}     {f} _   = z≤n
 injective⇒≤ {suc _} {zero}  {f} _   = contradiction (f zero) ¬Fin0
 injective⇒≤ {suc _} {suc _} {f} inj = s≤s (injective⇒≤ (λ eq →
   suc-injective (inj (punchOut-injective
-    (contraInjective _≡_ _≡_ inj 0≢1+n)
-    (contraInjective _≡_ _≡_ inj 0≢1+n) eq))))
+    (contraInjective inj 0≢1+n)
+    (contraInjective inj 0≢1+n) eq))))
 
 <⇒notInjective : ∀ {f : Fin m → Fin n} → n ℕ.< m → ¬ (Injective _≡_ _≡_ f)
 <⇒notInjective n<m inj = ℕₚ.≤⇒≯ (injective⇒≤ inj) n<m
diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
index c34e1b8904..7e7a3a090d 100644
--- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
@@ -28,7 +28,7 @@ open import Data.Product using (∃₂; _×_; _,_; <_,_>; proj₂; uncurry)
 
 open import Function.Base
 open import Function.Bundles using (_⤖_; _⇔_ ; mk⤖; mk⇔)
-
+open import Function.Consequences.Propositional using (strictlySurjective⇒surjective)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary using (Dec; does; _because_; yes; no; ¬_)
 open import Relation.Nullary.Decidable as Dec using (¬?)
@@ -345,7 +345,7 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
   toAny∘fromAny≗id (there p) = P.cong there (toAny∘fromAny≗id p)
 
   Sublist-[x]-bijection : ∀ {x xs} → (Sublist R [ x ] xs) ⤖ (Any (R x) xs)
-  Sublist-[x]-bijection = mk⤖ (toAny-injective , < fromAny , toAny∘fromAny≗id >)
+  Sublist-[x]-bijection = mk⤖ (toAny-injective , strictlySurjective⇒surjective < fromAny , toAny∘fromAny≗id >)
 
 ------------------------------------------------------------------------
 -- Relational properties
diff --git a/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda b/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda
index 78a365324b..f01fd90a48 100644
--- a/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda
@@ -20,14 +20,14 @@ open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Function.Base using (_∘_)
 open import Function.Bundles using (Surjection)
 open import Function.Definitions using (Surjective)
+open import Function.Consequences using (strictlySurjective⇒surjective)
 open import Level
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Binary.Properties.Setoid using (respʳ-flip)
 
 module Data.List.Relation.Unary.Enumerates.Setoid.Properties where
 
-open Setoid
 
 private
   variable
@@ -40,7 +40,7 @@ module _ (S : Setoid a ℓ₁) (T : Setoid b ℓ₂) (surj : Surjection S T) whe
   open Surjection surj
 
   map⁺ : ∀ {xs} → IsEnumeration S xs → IsEnumeration T (map to xs)
-  map⁺ _∈xs y with surjective y
+  map⁺ _∈xs y with strictlySurjective y
   ... | (x , fx≈y) = ∈-resp-≈ T fx≈y (∈-map⁺ S T cong (x ∈xs))
 
 ------------------------------------------------------------------------
@@ -84,7 +84,9 @@ module _ (S? : DecSetoid a ℓ₁) where
 -- lookup
 
 module _ (S : Setoid a ℓ₁) where
+  open Setoid S
 
   lookup-surjective : ∀ {xs} → IsEnumeration S xs →
-                      Surjective _≡_ (_≈_ S) (lookup xs)
-  lookup-surjective _∈xs y = index (y ∈xs) , sym S (lookup-index (y ∈xs))
+                      Surjective _≡_ _≈_ (lookup xs)
+  lookup-surjective _∈xs = strictlySurjective⇒surjective
+    trans (λ { P.refl → refl}) (λ y → index (y ∈xs) , sym (lookup-index (y ∈xs)))
diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda
index 3c362222ed..2294a08968 100644
--- a/src/Data/Nat/Binary/Properties.agda
+++ b/src/Data/Nat/Binary/Properties.agda
@@ -24,8 +24,8 @@ open import Data.Nat.Solver
 open import Data.Product using (_×_; _,_; proj₁; proj₂; ∃)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_∘_; _$_; id)
-open import Function.Definitions using (Injective)
-open import Function.Definitions.Core2 using (Surjective)
+open import Function.Definitions
+open import Function.Consequences.Propositional
 open import Level using (0ℓ)
 open import Relation.Binary
 open import Relation.Binary.Consequences
@@ -196,8 +196,8 @@ toℕ-injective {1+[2 x ]} {1+[2 y ]} 1+2xN≡1+2yN =  cong 1+[2_] x≡y
   xN≡yN   = ℕₚ.*-cancelˡ-≡ _ _ 2 2xN≡2yN
   x≡y     = toℕ-injective xN≡yN
 
-toℕ-surjective : Surjective _≡_ toℕ
-toℕ-surjective n = (fromℕ n , toℕ-fromℕ n)
+toℕ-surjective : Surjective _≡_ _≡_ toℕ
+toℕ-surjective = strictlySurjective⇒surjective (λ n → fromℕ n , toℕ-fromℕ n)
 
 toℕ-isRelHomomorphism : IsRelHomomorphism _≡_ _≡_ toℕ
 toℕ-isRelHomomorphism = record
@@ -215,6 +215,15 @@ fromℕ-injective {x} {y} f[x]≡f[y] = begin
 fromℕ-toℕ : fromℕ ∘ toℕ ≗ id
 fromℕ-toℕ = toℕ-injective ∘ toℕ-fromℕ ∘ toℕ
 
+toℕ-inverseˡ : Inverseˡ _≡_ _≡_ toℕ fromℕ
+toℕ-inverseˡ = strictlyInverseˡ⇒inverseˡ {f⁻¹ = fromℕ} toℕ toℕ-fromℕ
+
+toℕ-inverseʳ : Inverseʳ _≡_ _≡_ toℕ fromℕ
+toℕ-inverseʳ = strictlyInverseʳ⇒inverseʳ toℕ fromℕ-toℕ
+
+toℕ-inverseᵇ : Inverseᵇ _≡_ _≡_ toℕ fromℕ
+toℕ-inverseᵇ = toℕ-inverseˡ , toℕ-inverseʳ
+
 fromℕ-pred : ∀ n → fromℕ (ℕ.pred n) ≡ pred (fromℕ n)
 fromℕ-pred n = begin
   fromℕ (ℕ.pred n)        ≡⟨ cong (fromℕ ∘ ℕ.pred) (sym (toℕ-fromℕ n)) ⟩
diff --git a/src/Data/Nat/Binary/Subtraction.agda b/src/Data/Nat/Binary/Subtraction.agda
index 5ab5e243e0..a3e1de4a1b 100644
--- a/src/Data/Nat/Binary/Subtraction.agda
+++ b/src/Data/Nat/Binary/Subtraction.agda
@@ -109,8 +109,8 @@ toℕ-homo-∸ 1+[2 x ] 1+[2 y ] = begin
   where open ≡-Reasoning
 
 fromℕ-homo-∸ : ∀ m n → fromℕ (m ℕ.∸ n) ≡ (fromℕ m) ∸ (fromℕ n)
-fromℕ-homo-∸ = homomorphic₂-inv ∸-magma ℕₚ.∸-magma {toℕ}
-  (cong fromℕ) (toℕ-fromℕ , fromℕ-toℕ) toℕ-homo-∸
+fromℕ-homo-∸ = homomorphic₂-inv ∸-magma ℕₚ.∸-magma
+  (cong fromℕ) toℕ-inverseᵇ toℕ-homo-∸
 
 ------------------------------------------------------------------------
 -- Properties of _∸_ and _≤_/_<_
diff --git a/src/Data/Parity/Properties.agda b/src/Data/Parity/Properties.agda
index b9fb8a5eb7..574c9c68c1 100644
--- a/src/Data/Parity/Properties.agda
+++ b/src/Data/Parity/Properties.agda
@@ -15,7 +15,8 @@ open import Data.Parity.Base as ℙ using (Parity; 0ℙ; 1ℙ; _⁻¹; toSign; f
 open import Data.Product using (_,_)
 open import Data.Sign.Base as 𝕊
 open import Function.Base using (_$_; id)
-open import Function.Definitions using (Injective; Surjective)
+open import Function.Definitions
+open import Function.Consequences.Propositional
 open import Level using (0ℓ)
 open import Relation.Binary
   using (Decidable; DecidableEquality; Setoid; DecSetoid; IsDecEquivalence)
@@ -402,23 +403,19 @@ p+p≡0ℙ 1ℙ = refl
 ⁻¹-homo-opposite 0ℙ = refl
 ⁻¹-homo-opposite 1ℙ = refl
 
-toSign-inverts-fromSign : ∀ {p s} → toSign p ≡ s → fromSign s ≡ p
-toSign-inverts-fromSign {0ℙ} refl = refl
-toSign-inverts-fromSign {1ℙ} refl = refl
+toSign-inverseʳ : Inverseʳ _≡_ _≡_ toSign fromSign
+toSign-inverseʳ {0ℙ} refl = refl
+toSign-inverseʳ {1ℙ} refl = refl
 
-fromSign-inverts-toSign : ∀ {s p} → fromSign s ≡ p → toSign p ≡ s
-fromSign-inverts-toSign { + }  refl = refl
-fromSign-inverts-toSign { - } refl = refl
+toSign-inverseˡ : Inverseˡ _≡_ _≡_ toSign fromSign
+toSign-inverseˡ { + }  refl = refl
+toSign-inverseˡ { - } refl = refl
 
 toSign-injective : Injective _≡_ _≡_ toSign
-toSign-injective {p} {q} eq = begin
-  p                   ≡⟨ sym (toSign-inverts-fromSign {p} refl) ⟩
-  fromSign (toSign p) ≡⟨ cong fromSign eq ⟩
-  fromSign (toSign q) ≡⟨ toSign-inverts-fromSign {q} refl ⟩
-  q ∎ where open ≡-Reasoning
+toSign-injective = inverseʳ⇒injective toSign toSign-inverseʳ
 
 toSign-surjective : Surjective _≡_ _≡_ toSign
-toSign-surjective s = (fromSign s) , fromSign-inverts-toSign {s} refl
+toSign-surjective = inverseˡ⇒surjective toSign-inverseˡ
 
 toSign-isMagmaHomomorphism : IsMagmaHomomorphism ℙ.+-rawMagma 𝕊.*-rawMagma toSign
 toSign-isMagmaHomomorphism = record
@@ -477,7 +474,7 @@ toSign-isGroupIsomorphism = record
 
 
 ------------------------------------------------------------------------
--- relating Nat and Parity
+-- Relating Nat and Parity
 
 -- successor and (_⁻¹)
 
diff --git a/src/Data/Product/Algebra.agda b/src/Data/Product/Algebra.agda
index c64057dcc0..0b268b6ffd 100644
--- a/src/Data/Product/Algebra.agda
+++ b/src/Data/Product/Algebra.agda
@@ -29,13 +29,7 @@ import Function.Definitions as FuncDef
 private
   variable
     a b c d p : Level
-    A : Set a
-    B : Set b
-    C : Set c
-    D : Set d
-
-  module _ {A : Set a} {B : Set b} where
-    open FuncDef {A = A} {B} _≡_ _≡_
+    A B C D : Set a
 
 ------------------------------------------------------------------------
 -- Properties of Σ
@@ -56,8 +50,8 @@ private
 -- × is a congruence
 ×-cong : A ↔ B → C ↔ D → (A × C) ↔ (B × D)
 ×-cong i j = mk↔′ (map I.to J.to) (map I.from J.from)
-  (λ {(a , b) → cong₂ _,_ (I.inverseˡ a) (J.inverseˡ b)})
-  (λ {(a , b) → cong₂ _,_ (I.inverseʳ a) (J.inverseʳ b)})
+  (λ {(a , b) → cong₂ _,_ (I.strictlyInverseˡ a) (J.strictlyInverseˡ b)})
+  (λ {(a , b) → cong₂ _,_ (I.strictlyInverseʳ a) (J.strictlyInverseʳ b)})
   where module I = Inverse i; module J = Inverse j
 
 -- × is commutative.
diff --git a/src/Data/Sum/Algebra.agda b/src/Data/Sum/Algebra.agda
index f69988942b..ca96ac9c1c 100644
--- a/src/Data/Sum/Algebra.agda
+++ b/src/Data/Sum/Algebra.agda
@@ -29,14 +29,7 @@ import Function.Definitions as FuncDef
 private
   variable
     a b c d : Level
-    A : Set a
-    B : Set b
-    C : Set c
-    D : Set d
-
-  -- The module is needed because we need to pass `A` and `B` to `FuncDef`
-  module _ {A : Set a} {B : Set b} where
-    open FuncDef {A = A} {B} _≡_ _≡_
+    A B C D : Set a
 
   ♯ : {B : ⊥ {a} → Set b} → (w : ⊥) → B w
   ♯ ()
@@ -46,8 +39,8 @@ private
 
 ⊎-cong : A ↔ B → C ↔ D → (A ⊎ C) ↔ (B ⊎ D)
 ⊎-cong i j = mk↔′ (map I.to J.to) (map I.from J.from)
-  [ cong inj₁ ∘ I.inverseˡ , cong inj₂ ∘ J.inverseˡ ]
-  [ cong inj₁ ∘ I.inverseʳ , cong inj₂ ∘ J.inverseʳ ]
+  [ cong inj₁ ∘ I.strictlyInverseˡ , cong inj₂ ∘ J.strictlyInverseˡ ]
+  [ cong inj₁ ∘ I.strictlyInverseʳ , cong inj₂ ∘ J.strictlyInverseʳ ]
   where module I = Inverse i; module J = Inverse j
 
 -- ⊎ is commutative.
diff --git a/src/Data/Vec/N-ary.agda b/src/Data/Vec/N-ary.agda
index 197552d753..9220f86547 100644
--- a/src/Data/Vec/N-ary.agda
+++ b/src/Data/Vec/N-ary.agda
@@ -184,5 +184,5 @@ module _ (ext : ∀ {a b} → Extensionality a b) where
   Vec↔N-ary (suc n) = let open Inverse (Vec↔N-ary n) in
     mk↔′ (λ vxs x → to λ xs → vxs (x ∷ xs))
     (λ any xs → from (any (head xs)) (tail xs))
-    (λ any → ext λ x → inverseˡ _)
-    (λ vxs → ext λ where (x ∷ xs) → cong (λ f → f xs) (inverseʳ (λ ys → vxs (x ∷ ys))))
+    (λ any → ext λ x → strictlyInverseˡ _)
+    (λ vxs → ext λ where (x ∷ xs) → cong (λ f → f xs) (strictlyInverseʳ (λ ys → vxs (x ∷ ys))))
diff --git a/src/Data/Vec/Recursive.agda b/src/Data/Vec/Recursive.agda
index bd99c2064e..4c8796d016 100644
--- a/src/Data/Vec/Recursive.agda
+++ b/src/Data/Vec/Recursive.agda
@@ -29,7 +29,7 @@ open import Data.Unit.Polymorphic.Base using (⊤)
 open import Data.Unit.Polymorphic.Properties using (⊤↔⊤*)
 open import Data.Vec.Base as Vec using (Vec; _∷_)
 open import Data.Vec.N-ary using (N-ary)
-open import Function.Base using (_∘′_; _∘_; id)
+open import Function.Base using (_∘′_; _∘_; id; const)
 open import Function.Bundles using (_↔_; mk↔′; mk↔)
 open import Function.Properties.Inverse using (↔-isEquivalence; ↔-refl; ↔-sym; ↔-trans)
 open import Level using (Level; lift)
@@ -44,8 +44,8 @@ private
     B : Set b
     C : Set c
 
--- Types and patterns
 ------------------------------------------------------------------------
+-- Types and patterns
 
 infix 8 _^_
 _^_ : Set a → ℕ → Set a
@@ -61,8 +61,8 @@ a ∈[ 0    ] as               = ⊥
 a ∈[ 1    ] a′               = a ≡ a′
 a ∈[ suc n@(suc _) ] a′ , as = a ≡ a′ ⊎ a ∈[ n ] as
 
--- Basic operations
 ------------------------------------------------------------------------
+-- Basic operations
 
 cons : ∀ n → A → A ^ n → A ^ suc n
 cons 0       a _  = a
@@ -106,9 +106,8 @@ splitAt (suc m) n xs =
   let (ys , zs) = splitAt m n (tail (m Nat.+ n) xs) in
   cons m (head (m Nat.+ n) xs) ys , zs
 
-
--- Manipulating N-ary products
 ------------------------------------------------------------------------
+-- Manipulating N-ary products
 
 map : (A → B) → ∀ n → A ^ n → B ^ n
 map f 0      as       = lift tt
@@ -156,7 +155,7 @@ unzip : ∀ n → (A × B) ^ n → A ^ n × B ^ n
 unzip = unzipWith id
 
 lift↔ : ∀ n → A ↔ B → A ^ n ↔ B ^ n
-lift↔ 0               A↔B = mk↔ ((λ { [] → refl }) , (λ{ [] → refl }))
+lift↔ 0               A↔B = mk↔′ _ _ (const refl) (const refl)
 lift↔ 1               A↔B = A↔B
 lift↔ (suc n@(suc _)) A↔B = ×-cong A↔B (lift↔ n A↔B)
 
diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda
index d113f14858..1b92bee909 100644
--- a/src/Function/Bundles.agda
+++ b/src/Function/Bundles.agda
@@ -20,7 +20,7 @@
 module Function.Bundles where
 
 open import Function.Base using (_∘_)
-import Function.Definitions as FunctionDefinitions
+open import Function.Definitions
 import Function.Structures as FunctionStructures
 open import Level using (Level; _⊔_; suc)
 open import Data.Product.Base using (_,_; proj₁; proj₂)
@@ -28,6 +28,7 @@ open import Relation.Binary hiding (_⇔_)
 open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as ≡
+open import Function.Consequences.Propositional
 open Setoid using (isEquivalence)
 
 private
@@ -42,8 +43,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
 
   open Setoid From using () renaming (Carrier to A; _≈_ to _≈₁_)
   open Setoid To   using () renaming (Carrier to B; _≈_ to _≈₂_)
-  open FunctionDefinitions _≈₁_ _≈₂_
-  open FunctionStructures  _≈₁_ _≈₂_
+  open FunctionStructures _≈₁_ _≈₂_
 
 ------------------------------------------------------------------------
 -- Bundles with one element
@@ -53,7 +53,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
   record Func : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       to   : A → B
-      cong : to Preserves _≈₁_ ⟶ _≈₂_
+      cong : Congruent _≈₁_ _≈₂_ to
 
     isCongruent : IsCongruent to
     isCongruent = record
@@ -69,8 +69,8 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
   record Injection : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       to          : A → B
-      cong        : to Preserves _≈₁_ ⟶ _≈₂_
-      injective   : Injective to
+      cong        : Congruent _≈₁_ _≈₂_ to
+      injective   : Injective _≈₁_ _≈₂_ to
 
     function : Func
     function = record
@@ -91,8 +91,8 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
   record Surjection : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       to         : A → B
-      cong       : to Preserves _≈₁_ ⟶ _≈₂_
-      surjective : Surjective to
+      cong       : Congruent _≈₁_ _≈₂_ to
+      surjective : Surjective _≈₁_ _≈₂_ to
 
     to⁻ : B → A
     to⁻ = proj₁ ∘ surjective
@@ -104,25 +104,30 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
       ; isEquivalence₂ = isEquivalence To
       }
 
-    open IsCongruent isCongruent public using (module Eq₁; module Eq₂)
-
     isSurjection : IsSurjection to
     isSurjection = record
       { isCongruent = isCongruent
       ; surjective  = surjective
       }
 
+    open IsSurjection isSurjection public
+      using
+      ( module Eq₁
+      ; module Eq₂
+      ; strictlySurjective
+      )
+
 
   record Bijection : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       to        : A → B
-      cong      : to Preserves _≈₁_ ⟶ _≈₂_
-      bijective : Bijective to
+      cong      : Congruent _≈₁_ _≈₂_ to
+      bijective : Bijective _≈₁_ _≈₂_ to
 
-    injective : Injective to
+    injective : Injective _≈₁_ _≈₂_ to
     injective = proj₁ bijective
 
-    surjective : Surjective to
+    surjective : Surjective _≈₁_ _≈₂_ to
     surjective = proj₂ bijective
 
     injection : Injection
@@ -138,7 +143,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
       }
 
     open Injection  injection  public using (isInjection)
-    open Surjection surjection public using (isSurjection; to⁻)
+    open Surjection surjection public using (isSurjection; to⁻;  strictlySurjective)
 
     isBijection : IsBijection to
     isBijection = record
@@ -156,7 +161,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
     field
       to        : A → B
       from      : B → A
-      to-cong   : to Preserves _≈₁_ ⟶ _≈₂_
+      to-cong   : Congruent _≈₁_ _≈₂_ to
       from-cong : from Preserves _≈₂_ ⟶ _≈₁_
 
 
@@ -164,9 +169,9 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
     field
       to        : A → B
       from      : B → A
-      to-cong   : to Preserves _≈₁_ ⟶ _≈₂_
+      to-cong   : Congruent _≈₁_ _≈₂_ to
       from-cong : from Preserves _≈₂_ ⟶ _≈₁_
-      inverseˡ  : Inverseˡ to from
+      inverseˡ  : Inverseˡ _≈₁_ _≈₂_ to from
 
     isCongruent : IsCongruent to
     isCongruent = record
@@ -175,8 +180,6 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
       ; isEquivalence₂ = isEquivalence To
       }
 
-    open IsCongruent isCongruent public using (module Eq₁; module Eq₂)
-
     isLeftInverse : IsLeftInverse to from
     isLeftInverse = record
       { isCongruent = isCongruent
@@ -184,6 +187,9 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
       ; inverseˡ    = inverseˡ
       }
 
+    open IsLeftInverse isLeftInverse public
+      using (module Eq₁; module Eq₂; strictlyInverseˡ)
+
     equivalence : Equivalence
     equivalence = record
       { to-cong   = to-cong
@@ -195,9 +201,9 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
     field
       to        : A → B
       from      : B → A
-      to-cong   : to Preserves _≈₁_ ⟶ _≈₂_
+      to-cong   : Congruent _≈₁_ _≈₂_ to
       from-cong : from Preserves _≈₂_ ⟶ _≈₁_
-      inverseʳ  : Inverseʳ to from
+      inverseʳ  : Inverseʳ _≈₁_ _≈₂_ to from
 
     isCongruent : IsCongruent to
     isCongruent = record
@@ -213,6 +219,9 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
       ; inverseʳ    = inverseʳ
       }
 
+    open IsRightInverse isRightInverse public
+      using (module Eq₁; module Eq₂; strictlyInverseʳ)
+
     equivalence : Equivalence
     equivalence = record
       { to-cong   = to-cong
@@ -224,14 +233,14 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
     field
       to        : A → B
       from      : B → A
-      to-cong   : to Preserves _≈₁_ ⟶ _≈₂_
-      from-cong : from Preserves _≈₂_ ⟶ _≈₁_
-      inverse   : Inverseᵇ to from
+      to-cong   : Congruent _≈₁_ _≈₂_ to
+      from-cong : Congruent _≈₂_ _≈₁_ from
+      inverse   : Inverseᵇ _≈₁_ _≈₂_ to from
 
-    inverseˡ : Inverseˡ to from
+    inverseˡ : Inverseˡ _≈₁_ _≈₂_ to from
     inverseˡ = proj₁ inverse
 
-    inverseʳ : Inverseʳ to from
+    inverseʳ : Inverseʳ _≈₁_ _≈₂_ to from
     inverseʳ = proj₂ inverse
 
     leftInverse : LeftInverse
@@ -248,8 +257,8 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
       ; inverseʳ  = inverseʳ
       }
 
-    open LeftInverse leftInverse   public using (isLeftInverse)
-    open RightInverse rightInverse public using (isRightInverse)
+    open LeftInverse leftInverse   public using (isLeftInverse; strictlyInverseˡ)
+    open RightInverse rightInverse public using (isRightInverse; strictlyInverseʳ)
 
     isInverse : IsInverse to from
     isInverse = record
@@ -268,21 +277,21 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
       to         : A → B
       from₁      : B → A
       from₂      : B → A
-      to-cong    : to Preserves _≈₁_ ⟶ _≈₂_
-      from₁-cong : from₁ Preserves _≈₂_ ⟶ _≈₁_
-      from₂-cong : from₂ Preserves _≈₂_ ⟶ _≈₁_
+      to-cong    : Congruent _≈₁_ _≈₂_ to
+      from₁-cong : Congruent _≈₂_ _≈₁_ from₁
+      from₂-cong : Congruent _≈₂_ _≈₁_ from₂
 
 
   record BiInverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
     field
-      to         : A → B
-      from₁        : B → A
-      from₂        : B → A
-      to-cong     : to Preserves _≈₁_ ⟶ _≈₂_
-      from₁-cong     : from₁ Preserves _≈₂_ ⟶ _≈₁_
-      from₂-cong     : from₂ Preserves _≈₂_ ⟶ _≈₁_
-      inverseˡ  : Inverseˡ to from₁
-      inverseʳ  : Inverseʳ to from₂
+      to          : A → B
+      from₁       : B → A
+      from₂       : B → A
+      to-cong     : Congruent _≈₁_ _≈₂_ to
+      from₁-cong  : Congruent _≈₂_ _≈₁_ from₁
+      from₂-cong  : Congruent _≈₂_ _≈₁_ from₂
+      inverseˡ  : Inverseˡ _≈₁_ _≈₂_ to from₁
+      inverseʳ  : Inverseʳ _≈₁_ _≈₂_ to from₂
 
     to-isCongruent : IsCongruent to
     to-isCongruent = record
@@ -345,29 +354,27 @@ A ↔ B = Inverse (≡.setoid A) (≡.setoid B)
 
 module _ {A : Set a} {B : Set b} where
 
-  open FunctionDefinitions {A = A} {B} _≡_ _≡_
-
   mk⟶ : (A → B) → A ⟶ B
   mk⟶ to = record
     { to        = to
     ; cong      = ≡.cong to
     }
 
-  mk↣ : ∀ {to : A → B} → Injective to → A ↣ B
+  mk↣ : ∀ {to : A → B} → Injective _≡_ _≡_ to → A ↣ B
   mk↣ {to} inj = record
     { to         = to
     ; cong      = ≡.cong to
     ; injective = inj
     }
 
-  mk↠ : ∀ {to : A → B} → Surjective to → A ↠ B
+  mk↠ : ∀ {to : A → B} → Surjective _≡_ _≡_ to → A ↠ B
   mk↠ {to} surj = record
     { to         = to
     ; cong       = ≡.cong to
     ; surjective = surj
     }
 
-  mk⤖ : ∀ {to : A → B} → Bijective to → A ⤖ B
+  mk⤖ : ∀ {to : A → B} → Bijective _≡_ _≡_ to → A ⤖ B
   mk⤖ {to} bij = record
     { to        = to
     ; cong      = ≡.cong to
@@ -382,7 +389,7 @@ module _ {A : Set a} {B : Set b} where
     ; from-cong = ≡.cong from
     }
 
-  mk↩ : ∀ {to : A → B} {from : B → A} → Inverseˡ to from → A ↩ B
+  mk↩ : ∀ {to : A → B} {from : B → A} → Inverseˡ _≡_ _≡_ to from → A ↩ B
   mk↩ {to} {from} invˡ = record
     { to        = to
     ; from      = from
@@ -391,7 +398,7 @@ module _ {A : Set a} {B : Set b} where
     ; inverseˡ  = invˡ
     }
 
-  mk↪ : ∀ {to : A → B} {from : B → A} → Inverseʳ to from → A ↪ B
+  mk↪ : ∀ {to : A → B} {from : B → A} → Inverseʳ _≡_ _≡_ to from → A ↪ B
   mk↪ {to} {from} invʳ = record
     { to        = to
     ; from      = from
@@ -401,7 +408,7 @@ module _ {A : Set a} {B : Set b} where
     }
 
   mk↩↪ : ∀ {to : A → B} {from₁ : B → A} {from₂ : B → A} →
-         Inverseˡ to from₁ → Inverseʳ to from₂ → A ↩↪ B
+         Inverseˡ _≡_ _≡_ to from₁ → Inverseʳ _≡_ _≡_ to from₂ → A ↩↪ B
   mk↩↪ {to} {from₁} {from₂} invˡ invʳ = record
     { to         = to
     ; from₁      = from₁
@@ -413,7 +420,7 @@ module _ {A : Set a} {B : Set b} where
     ; inverseʳ   = invʳ
     }
 
-  mk↔ : ∀ {to : A → B} {from : B → A} → Inverseᵇ to from → A ↔ B
+  mk↔ : ∀ {to : A → B} {from : B → A} → Inverseᵇ _≡_ _≡_ to from → A ↔ B
   mk↔ {to} {from} inv = record
     { to        = to
     ; from      = from
@@ -422,6 +429,13 @@ module _ {A : Set a} {B : Set b} where
     ; inverse   = inv
     }
 
-  -- Sometimes the implicit arguments above cannot be inferred
-  mk↔′ : ∀ (to : A → B) (from : B → A) → Inverseˡ to from → Inverseʳ to from → A ↔ B
-  mk↔′ to from invˡ invʳ = mk↔ {to = to} {from = from} (invˡ , invʳ)
+  -- Strict variant of the above.
+  mk↔′ : ∀ (to : A → B) (from : B → A) →
+          StrictlyInverseˡ _≡_ to from →
+          StrictlyInverseʳ _≡_ to from →
+          A ↔ B
+  mk↔′ to from invˡ invʳ = mk↔ {to} {from}
+    ( strictlyInverseˡ⇒inverseˡ to invˡ
+    , strictlyInverseʳ⇒inverseʳ to invʳ
+    )
+
diff --git a/src/Function/Consequences.agda b/src/Function/Consequences.agda
index e8c6a0f498..242aa3d289 100644
--- a/src/Function/Consequences.agda
+++ b/src/Function/Consequences.agda
@@ -1,55 +1,113 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Relationships between properties of functions
+-- Relationships between properties of functions. See
+-- `Function.Consequences.Propositional` for specialisations to
+-- propositional equality.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
 module Function.Consequences where
 
-open import Data.Product.Base using (_,_)
+open import Data.Product.Base as Prod
 open import Function.Definitions
-open import Level using (Level)
-open import Relation.Binary
-import Relation.Binary.Reasoning.Setoid as SetoidReasoning
+open import Level
+open import Relation.Binary.Core
+open import Relation.Binary.Definitions
 open import Relation.Nullary.Negation.Core using (¬_; contraposition)
 
 private
   variable
     a b ℓ₁ ℓ₂ : Level
-    A : Set a
-    B : Set b
+    A B : Set a
+    ≈₁ ≈₂ : Rel A ℓ₁
+    f f⁻¹ : A → B
 
-module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) {f f⁻¹} where
+------------------------------------------------------------------------
+-- Injective
+
+contraInjective : Injective ≈₁ ≈₂ f →
+                  ∀ {x y} → ¬ (≈₁ x y) → ¬ (≈₂ (f x) (f y))
+contraInjective inj p = contraposition inj p
+
+------------------------------------------------------------------------
+-- Inverseˡ
 
-  inverseˡ⇒surjective : Inverseˡ ≈₁ ≈₂ f f⁻¹ → Surjective ≈₁ ≈₂ f
-  inverseˡ⇒surjective invˡ y = (f⁻¹ y , invˡ y)
+inverseˡ⇒surjective : ∀ (≈₂ : Rel B ℓ₂) →
+                      Inverseˡ ≈₁ ≈₂ f f⁻¹ →
+                      Surjective ≈₁ ≈₂ f
+inverseˡ⇒surjective ≈₂ invˡ y = (_ , invˡ)
 
-  inverseʳ⇒surjective : Inverseʳ ≈₁ ≈₂ f f⁻¹ → Surjective ≈₂ ≈₁ f⁻¹
-  inverseʳ⇒surjective invʳ y = (f y , invʳ y)
+------------------------------------------------------------------------
+-- Inverseʳ
+
+inverseʳ⇒injective : ∀ (≈₂ : Rel B ℓ₂) f →
+                     Reflexive ≈₂ →
+                     Symmetric ≈₁ →
+                     Transitive ≈₁ →
+                     Inverseʳ ≈₁ ≈₂ f f⁻¹ →
+                     Injective ≈₁ ≈₂ f
+inverseʳ⇒injective ≈₂ f refl sym trans invʳ {x} {y} fx≈fy =
+  trans (sym (invʳ refl)) (invʳ fx≈fy)
 
-module _ (From : Setoid a ℓ₁) {≈₂ : Rel B ℓ₂} where
+------------------------------------------------------------------------
+-- Inverseᵇ
 
-  open Setoid From using () renaming (Carrier to A; _≈_ to ≈₁)
+inverseᵇ⇒bijective : ∀ (≈₂ : Rel B ℓ₂) →
+                     Reflexive ≈₂ →
+                     Symmetric ≈₁ →
+                     Transitive ≈₁ →
+                     Inverseᵇ ≈₁ ≈₂ f f⁻¹ →
+                     Bijective ≈₁ ≈₂ f
+inverseᵇ⇒bijective {f = f} ≈₂ refl sym trans (invˡ , invʳ) =
+  (inverseʳ⇒injective ≈₂ f refl sym trans invʳ , inverseˡ⇒surjective ≈₂ invˡ)
 
-  inverseʳ⇒injective : ∀ {f f⁻¹} → Congruent ≈₂ ≈₁ f⁻¹ →
-                       Inverseʳ ≈₁ ≈₂ f f⁻¹ → Injective ≈₁ ≈₂ f
-  inverseʳ⇒injective {f} {f⁻¹} cong₂ invʳ {x} {y} x≈y = begin
-    x         ≈˘⟨ invʳ x ⟩
-    f⁻¹ (f x) ≈⟨  cong₂ x≈y ⟩
-    f⁻¹ (f y) ≈⟨  invʳ y ⟩
-    y         ∎
-    where open SetoidReasoning From
+------------------------------------------------------------------------
+-- StrictlySurjective
 
-  inverseᵇ⇒bijective : ∀ {f f⁻¹} → Congruent ≈₂ ≈₁ f⁻¹ → Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Bijective ≈₁ ≈₂ f
-  inverseᵇ⇒bijective cong₂ (invˡ , invʳ) =
-    (inverseʳ⇒injective cong₂ invʳ , inverseˡ⇒surjective ≈₁ ≈₂ invˡ)
+surjective⇒strictlySurjective : ∀ (≈₂ : Rel B ℓ₂) →
+                                 Reflexive ≈₁ →
+                                 Surjective ≈₁ ≈₂ f →
+                                 StrictlySurjective ≈₂ f
+surjective⇒strictlySurjective _ refl surj x =
+  Prod.map₂ (λ v → v refl) (surj x)
+
+strictlySurjective⇒surjective : Transitive ≈₂ →
+                                 Congruent ≈₁ ≈₂ f →
+                                 StrictlySurjective ≈₂ f →
+                                 Surjective ≈₁ ≈₂ f
+strictlySurjective⇒surjective trans cong surj x =
+  Prod.map₂ (λ fy≈x z≈y → trans (cong z≈y) fy≈x) (surj x)
+
+------------------------------------------------------------------------
+-- StrictlyInverseˡ
+
+inverseˡ⇒strictlyInverseˡ : ∀ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) →
+                            Reflexive ≈₁ →
+                            Inverseˡ ≈₁ ≈₂ f f⁻¹ →
+                            StrictlyInverseˡ ≈₂ f f⁻¹
+inverseˡ⇒strictlyInverseˡ _ _ refl sinv x = sinv refl
+
+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ʳ
 
-module _
-  {f : A → B} (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂)
-  where
+inverseʳ⇒strictlyInverseʳ : ∀ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) →
+                            Reflexive ≈₂ →
+                            Inverseʳ ≈₁ ≈₂ f f⁻¹ →
+                            StrictlyInverseʳ ≈₁ f f⁻¹
+inverseʳ⇒strictlyInverseʳ _ _ refl sinv x = sinv refl
 
-  contraInjective : Injective _≈₁_ _≈₂_ f →
-                    ∀ {x y} → ¬ (x ≈₁ y) → ¬ (f x ≈₂ f y)
-  contraInjective inj p = contraposition inj p
+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)
diff --git a/src/Function/Consequences/Propositional.agda b/src/Function/Consequences/Propositional.agda
new file mode 100644
index 0000000000..d6067a7702
--- /dev/null
+++ b/src/Function/Consequences/Propositional.agda
@@ -0,0 +1,91 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Relationships between properties of functions where the equality
+-- over both the domain and codomain is assumed to be _≡_
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Function.Consequences.Propositional where
+
+open import Function.Definitions
+open import Level
+open import Relation.Nullary.Negation.Core using (contraposition)
+open import Relation.Binary.PropositionalEquality.Core
+  using (_≡_; _≢_; refl; sym; trans; cong)
+
+import Function.Consequences as C
+
+private
+  variable
+    a b ℓ₁ ℓ₂ : Level
+    A B : Set a
+    f f⁻¹ : A → B
+
+------------------------------------------------------------------------
+-- Injective
+
+contraInjective : Injective _≡_ _≡_ f →
+                  ∀ {x y} → x ≢ y → f x ≢ f y
+contraInjective inj p = contraposition inj p
+
+------------------------------------------------------------------------
+-- Inverseˡ
+
+inverseˡ⇒surjective : Inverseˡ _≡_ _≡_ f f⁻¹ → Surjective _≡_ _≡_ f
+inverseˡ⇒surjective = C.inverseˡ⇒surjective _≡_
+
+------------------------------------------------------------------------
+-- Inverseʳ
+
+inverseʳ⇒injective : ∀ f →
+                     Inverseʳ _≡_ _≡_ f f⁻¹ →
+                     Injective _≡_ _≡_ f
+inverseʳ⇒injective f = C.inverseʳ⇒injective _≡_ f refl sym trans
+
+------------------------------------------------------------------------
+-- Inverseᵇ
+
+inverseᵇ⇒bijective : Inverseᵇ _≡_ _≡_ f f⁻¹ → Bijective _≡_ _≡_ f
+inverseᵇ⇒bijective = C.inverseᵇ⇒bijective _≡_ refl sym trans
+
+------------------------------------------------------------------------
+-- StrictlySurjective
+
+surjective⇒strictlySurjective : Surjective _≡_ _≡_ f →
+                                 StrictlySurjective _≡_ f
+surjective⇒strictlySurjective =
+  C.surjective⇒strictlySurjective _≡_ refl
+
+strictlySurjective⇒surjective : StrictlySurjective _≡_ f →
+                                 Surjective _≡_ _≡_ f
+strictlySurjective⇒surjective =
+  C.strictlySurjective⇒surjective trans (cong _)
+
+------------------------------------------------------------------------
+-- StrictlyInverseˡ
+
+inverseˡ⇒strictlyInverseˡ : Inverseˡ _≡_ _≡_ f f⁻¹ →
+                            StrictlyInverseˡ _≡_ f f⁻¹
+inverseˡ⇒strictlyInverseˡ =
+  C.inverseˡ⇒strictlyInverseˡ _≡_ _≡_ refl
+
+strictlyInverseˡ⇒inverseˡ : ∀ f →
+                            StrictlyInverseˡ _≡_ f f⁻¹ →
+                            Inverseˡ _≡_ _≡_ f f⁻¹
+strictlyInverseˡ⇒inverseˡ f =
+  C.strictlyInverseˡ⇒inverseˡ trans (cong f)
+
+------------------------------------------------------------------------
+-- StrictlyInverseʳ
+
+inverseʳ⇒strictlyInverseʳ : Inverseʳ _≡_ _≡_ f f⁻¹ →
+                            StrictlyInverseʳ _≡_ f f⁻¹
+inverseʳ⇒strictlyInverseʳ = C.inverseʳ⇒strictlyInverseʳ _≡_ _≡_ refl
+
+strictlyInverseʳ⇒inverseʳ : ∀ f →
+                            StrictlyInverseʳ _≡_ f f⁻¹ →
+                            Inverseʳ _≡_ _≡_ f f⁻¹
+strictlyInverseʳ⇒inverseʳ {f⁻¹ = f⁻¹} _ =
+  C.strictlyInverseʳ⇒inverseʳ trans (cong f⁻¹)
diff --git a/src/Function/Construct/Composition.agda b/src/Function/Construct/Composition.agda
index 269448eaba..b745daa8e6 100644
--- a/src/Function/Construct/Composition.agda
+++ b/src/Function/Construct/Composition.agda
@@ -8,14 +8,11 @@
 
 module Function.Construct.Composition where
 
-open import Data.Product.Base using (_,_)
+open import Data.Product.Base as Product using (_,_)
 open import Function.Base using (_∘_)
 open import Function.Bundles
-  using (Func; Injection; Surjection; Bijection; Equivalence; LeftInverse; RightInverse; Inverse; _⟶_; _↣_; _↠_; _⤖_; _⇔_; _↩_; _↪_; _↔_)
 open import Function.Definitions
-  using (Congruent; Injective; Surjective; Bijective; Inverseˡ; Inverseʳ; Inverseᵇ)
 open import Function.Structures
-  using (IsCongruent; IsInjection; IsSurjection; IsBijection; IsLeftInverse; IsRightInverse; IsInverse)
 open import Level using (Level)
 open import Relation.Binary hiding (_⇔_; IsEquivalence)
 
@@ -39,39 +36,31 @@ module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) (≈₃ : Rel C ℓ₃)
               Injective ≈₁ ≈₃ (g ∘ f)
   injective f-inj g-inj = f-inj ∘ g-inj
 
-  surjective : Transitive ≈₃ → Congruent ≈₂ ≈₃ g →
-               Surjective ≈₁ ≈₂ f → Surjective ≈₂ ≈₃ g →
+  surjective : Surjective ≈₁ ≈₂ f → Surjective ≈₂ ≈₃ g →
                Surjective ≈₁ ≈₃ (g ∘ f)
-  surjective trans g-cong f-sur g-sur x with g-sur x
-  ... | y , fy≈x  with f-sur y
-  ...   | z , fz≈y = z , trans (g-cong fz≈y) fy≈x
+  surjective f-sur g-sur x with g-sur x
+  ... | y , gproof with f-sur y
+  ...   | z , fproof = z , gproof ∘ fproof
 
-  bijective : Transitive ≈₃ → Congruent ≈₂ ≈₃ g →
-              Bijective ≈₁ ≈₂ f → Bijective ≈₂ ≈₃ g →
+  bijective : Bijective ≈₁ ≈₂ f → Bijective ≈₂ ≈₃ g →
               Bijective ≈₁ ≈₃ (g ∘ f)
-  bijective trans g-cong (f-inj , f-sur) (g-inj , g-sur) =
-    injective f-inj g-inj , surjective trans g-cong f-sur g-sur
+  bijective = Product.zip′ injective surjective
 
 module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) (≈₃ : Rel C ℓ₃)
-         (f : A → B) {f⁻¹ : B → A} {g : B → C} (g⁻¹ : C → B)
+         {f : A → B} {f⁻¹ : B → A} {g : B → C} {g⁻¹ : C → B}
          where
 
-  inverseˡ : Transitive ≈₃ → Congruent ≈₂ ≈₃ g →
-             Inverseˡ ≈₁ ≈₂ f f⁻¹ → Inverseˡ ≈₂ ≈₃ g g⁻¹ →
+  inverseˡ : Inverseˡ ≈₁ ≈₂ f f⁻¹ → Inverseˡ ≈₂ ≈₃ g g⁻¹ →
              Inverseˡ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
-  inverseˡ trn g-cong f-inv g-inv x = trn (g-cong (f-inv _)) (g-inv x)
+  inverseˡ f-inv g-inv = g-inv ∘ f-inv
 
-  inverseʳ : Transitive ≈₁ → Congruent ≈₂ ≈₁ f⁻¹ →
-             Inverseʳ ≈₁ ≈₂ f f⁻¹ → Inverseʳ ≈₂ ≈₃ g g⁻¹ →
+  inverseʳ : Inverseʳ ≈₁ ≈₂ f f⁻¹ → Inverseʳ ≈₂ ≈₃ g g⁻¹ →
              Inverseʳ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
-  inverseʳ trn f⁻¹-cong f-inv g-inv x = trn (f⁻¹-cong (g-inv _)) (f-inv x)
+  inverseʳ f-inv g-inv = f-inv ∘ g-inv
 
-  inverseᵇ : Transitive ≈₁ → Transitive ≈₃ →
-             Congruent ≈₂ ≈₃ g → Congruent ≈₂ ≈₁ f⁻¹ →
-             Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Inverseᵇ ≈₂ ≈₃ g g⁻¹ →
+  inverseᵇ : Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Inverseᵇ ≈₂ ≈₃ g g⁻¹ →
              Inverseᵇ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
-  inverseᵇ trn₁ trn₃ g-cong f⁻¹-cong (f-invˡ , f-invʳ) (g-invˡ , g-invʳ) =
-    inverseˡ trn₃ g-cong f-invˡ g-invˡ , inverseʳ trn₁ f⁻¹-cong f-invʳ g-invʳ
+  inverseᵇ = Product.zip′ inverseˡ inverseʳ
 
 ------------------------------------------------------------------------
 -- Structures
@@ -99,14 +88,14 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {≈₃ : Rel C ℓ₃}
                  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
+    ; surjective  = surjective ≈₁ ≈₂ ≈₃ F.surjective G.surjective
     } 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
+    ; surjective  = surjective ≈₁ ≈₂ ≈₃ F.surjective G.surjective
     } where module F = IsBijection f-bij; module G = IsBijection g-bij
 
 module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {≈₃ : Rel C ℓ₃}
@@ -117,23 +106,23 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {≈₃ : Rel C ℓ₃}
                   IsLeftInverse ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
   isLeftInverse f-invˡ g-invˡ = record
     { isCongruent = isCongruent F.isCongruent G.isCongruent
-    ; from-cong       = congruent ≈₃ ≈₂ ≈₁ G.from-cong F.from-cong
-    ; inverseˡ    = inverseˡ ≈₁ ≈₂ ≈₃ f _ G.Eq₂.trans G.to-cong F.inverseˡ G.inverseˡ
+    ; from-cong   = congruent ≈₃ ≈₂ ≈₁ G.from-cong F.from-cong
+    ; inverseˡ    = inverseˡ ≈₁ ≈₂ ≈₃ F.inverseˡ G.inverseˡ
     } 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
-    ; from-cong       = congruent ≈₃ ≈₂ ≈₁ G.from-cong F.from-cong
-    ; inverseʳ    = inverseʳ ≈₁ ≈₂ ≈₃ _ g⁻¹ F.Eq₁.trans F.from-cong F.inverseʳ G.inverseʳ
+    ; from-cong   = congruent ≈₃ ≈₂ ≈₁ G.from-cong F.from-cong
+    ; inverseʳ    = inverseʳ ≈₁ ≈₂ ≈₃ F.inverseʳ G.inverseʳ
     } 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.from-cong F.inverseʳ G.inverseʳ
+    ; inverseʳ      = inverseʳ ≈₁ ≈₂ ≈₃ F.inverseʳ G.inverseʳ
     } where module F = IsInverse f-inv; module G = IsInverse g-inv
 
 ------------------------------------------------------------------------
@@ -159,15 +148,15 @@ module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} {T : Setoid c ℓ₃} where
   surjection : Surjection R S → Surjection S T → Surjection R T
   surjection surj₁ surj₂ = record
     { to         = G.to ∘ F.to
-    ; cong       = congruent (≈ R) (≈ S) (≈ T) F.cong G.cong
-    ; surjective = surjective (≈ R) (≈ S) (≈ T) G.Eq₂.trans G.cong F.surjective G.surjective
+    ; cong       = congruent  (≈ R) (≈ S) (≈ T) F.cong G.cong
+    ; surjective = surjective (≈ R) (≈ S) (≈ T) F.surjective G.surjective
     } where module F = Surjection surj₁; module G = Surjection surj₂
 
   bijection : Bijection R S → Bijection S T → Bijection R T
   bijection bij₁ bij₂ = record
     { to        = G.to ∘ F.to
     ; cong      = congruent (≈ R) (≈ S) (≈ T) F.cong G.cong
-    ; bijective = bijective (≈ R) (≈ S) (≈ T) (trans T) G.cong F.bijective G.bijective
+    ; bijective = bijective (≈ R) (≈ S) (≈ T) F.bijective G.bijective
     } where module F = Bijection bij₁; module G = Bijection bij₂
 
   equivalence : Equivalence R S → Equivalence S T → Equivalence R T
@@ -184,7 +173,7 @@ module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} {T : Setoid c ℓ₃} where
     ; from      = F.from ∘ G.from
     ; to-cong   = congruent (≈ R) (≈ S) (≈ T) F.to-cong G.to-cong
     ; from-cong = congruent (≈ T) (≈ S) (≈ R) G.from-cong F.from-cong
-    ; inverseˡ  = inverseˡ  (≈ R) (≈ S) (≈ T) F.to _ (trans T) G.to-cong F.inverseˡ G.inverseˡ
+    ; inverseˡ  = inverseˡ  (≈ R) (≈ S) (≈ T) F.inverseˡ G.inverseˡ
     } where module F = LeftInverse invˡ₁; module G = LeftInverse invˡ₂
 
   rightInverse : RightInverse R S → RightInverse S T → RightInverse R T
@@ -193,7 +182,7 @@ module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} {T : Setoid c ℓ₃} where
     ; from      = F.from ∘ G.from
     ; to-cong   = congruent (≈ R) (≈ S) (≈ T) F.to-cong G.to-cong
     ; from-cong = congruent (≈ T) (≈ S) (≈ R) G.from-cong F.from-cong
-    ; inverseʳ  = inverseʳ  (≈ R) (≈ S) (≈ T) _ G.from (trans R) F.from-cong F.inverseʳ G.inverseʳ
+    ; inverseʳ  = inverseʳ  (≈ R) (≈ S) (≈ T) F.inverseʳ G.inverseʳ
     } where module F = RightInverse invʳ₁; module G = RightInverse invʳ₂
 
   inverse : Inverse R S → Inverse S T → Inverse R T
@@ -202,7 +191,7 @@ module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} {T : Setoid c ℓ₃} where
     ; from      = F.from ∘ G.from
     ; to-cong   = congruent (≈ R) (≈ S) (≈ T) F.to-cong G.to-cong
     ; from-cong = congruent (≈ T) (≈ S) (≈ R) G.from-cong F.from-cong
-    ; inverse   = inverseᵇ  (≈ R) (≈ S) (≈ T) _ G.from (trans R) (trans T) G.to-cong F.from-cong F.inverse G.inverse
+    ; inverse   = inverseᵇ  (≈ R) (≈ S) (≈ T) F.inverse G.inverse
     } where module F = Inverse inv₁; module G = Inverse inv₂
 
 ------------------------------------------------------------------------
diff --git a/src/Function/Construct/Identity.agda b/src/Function/Construct/Identity.agda
index bec0ecd3d6..e4ec7e3d3e 100644
--- a/src/Function/Construct/Identity.agda
+++ b/src/Function/Construct/Identity.agda
@@ -28,28 +28,28 @@ private
 
 module _ (_≈_ : Rel A ℓ) where
 
-  open Definitions _≈_ _≈_
+  open Definitions
 
-  congruent : Congruent id
+  congruent : Congruent _≈_ _≈_ id
   congruent = id
 
-  injective : Injective id
+  injective : Injective _≈_ _≈_ id
   injective = id
 
-  surjective : Reflexive _≈_ → Surjective id
-  surjective refl x = x , refl
+  surjective : Surjective _≈_ _≈_ id
+  surjective x = x , id
 
-  bijective : Reflexive _≈_ → Bijective id
-  bijective refl = injective , surjective refl
+  bijective : Bijective _≈_ _≈_ id
+  bijective = injective , surjective
 
-  inverseˡ : Reflexive _≈_ → Inverseˡ id id
-  inverseˡ refl x = refl
+  inverseˡ : Inverseˡ _≈_ _≈_ id id
+  inverseˡ = id
 
-  inverseʳ : Reflexive _≈_ → Inverseʳ id id
-  inverseʳ refl x = refl
+  inverseʳ : Inverseʳ _≈_ _≈_ id id
+  inverseʳ = id
 
-  inverseᵇ : Reflexive _≈_ → Inverseᵇ id id
-  inverseᵇ refl = inverseˡ refl , inverseʳ refl
+  inverseᵇ : Inverseᵇ _≈_ _≈_ id id
+  inverseᵇ = inverseˡ , inverseʳ
 
 ------------------------------------------------------------------------
 -- Structures
@@ -75,33 +75,33 @@ module _ {_≈_ : Rel A ℓ} (isEq : B.IsEquivalence _≈_) where
   isSurjection : IsSurjection id
   isSurjection = record
     { isCongruent = isCongruent
-    ; surjective  = surjective _≈_ refl
+    ; surjective  = surjective _≈_
     }
 
   isBijection : IsBijection id
   isBijection = record
     { isInjection = isInjection
-    ; surjective  = surjective _≈_ refl
+    ; surjective  = surjective _≈_
     }
 
   isLeftInverse : IsLeftInverse id id
   isLeftInverse = record
     { isCongruent = isCongruent
     ; from-cong   = id
-    ; inverseˡ    = inverseˡ _≈_ refl
+    ; inverseˡ    = inverseˡ _≈_
     }
 
   isRightInverse : IsRightInverse id id
   isRightInverse = record
     { isCongruent = isCongruent
     ; from-cong   = id
-    ; inverseʳ    = inverseʳ _≈_ refl
+    ; inverseʳ    = inverseʳ _≈_
     }
 
   isInverse : IsInverse id id
   isInverse = record
     { isLeftInverse = isLeftInverse
-    ; inverseʳ      = inverseʳ _≈_ refl
+    ; inverseʳ      = inverseʳ _≈_
     }
 
 ------------------------------------------------------------------------
@@ -128,14 +128,14 @@ module _ (S : Setoid a ℓ) where
   surjection = record
     { to         = id
     ; cong       = id
-    ; surjective = surjective _≈_ refl
+    ; surjective = surjective _≈_
     }
 
   bijection : Bijection S S
   bijection = record
     { to        = id
     ; cong      = id
-    ; bijective = bijective _≈_ refl
+    ; bijective = bijective _≈_
     }
 
   equivalence : Equivalence S S
@@ -152,7 +152,7 @@ module _ (S : Setoid a ℓ) where
     ; from      = id
     ; to-cong   = id
     ; from-cong = id
-    ; inverseˡ  = inverseˡ _≈_ refl
+    ; inverseˡ  = inverseˡ _≈_
     }
 
   rightInverse : RightInverse S S
@@ -161,7 +161,7 @@ module _ (S : Setoid a ℓ) where
     ; from      = id
     ; to-cong   = id
     ; from-cong = id
-    ; inverseʳ  = inverseʳ _≈_ refl
+    ; inverseʳ  = inverseʳ _≈_
     }
 
   inverse : Inverse S S
@@ -170,7 +170,7 @@ module _ (S : Setoid a ℓ) where
     ; from      = id
     ; to-cong   = id
     ; from-cong = id
-    ; inverse   = inverseᵇ _≈_ refl
+    ; inverse   = inverseᵇ _≈_
     }
 
 ------------------------------------------------------------------------
diff --git a/src/Function/Construct/Symmetry.agda b/src/Function/Construct/Symmetry.agda
index 14a7adc466..834ee0d4fa 100644
--- a/src/Function/Construct/Symmetry.agda
+++ b/src/Function/Construct/Symmetry.agda
@@ -18,9 +18,10 @@ open import Function.Bundles
   using (Bijection; Equivalence; LeftInverse; RightInverse; Inverse; _⤖_; _⇔_; _↩_; _↪_; _↔_)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
-open import Relation.Binary.Definitions using (Symmetric; Transitive)
+open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.PropositionalEquality
+  using (_≡_; cong; setoid)
 
 private
   variable
@@ -38,18 +39,19 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B}
     f⁻¹      = proj₁ ∘ surj
     f∘f⁻¹≡id = proj₂ ∘ surj
 
-  injective : Symmetric ≈₂ → Transitive ≈₂ → Congruent ≈₁ ≈₂ f → Injective ≈₂ ≈₁ f⁻¹
-  injective sym trans cong gx≈gy = trans (trans (sym (f∘f⁻¹≡id _)) (cong gx≈gy)) (f∘f⁻¹≡id _)
+  injective : Reflexive ≈₁ → Symmetric ≈₂ → Transitive ≈₂ →
+              Congruent ≈₁ ≈₂ f → Injective ≈₂ ≈₁ f⁻¹
+  injective refl sym trans cong gx≈gy =
+    trans (trans (sym (f∘f⁻¹≡id _ refl)) (cong gx≈gy)) (f∘f⁻¹≡id _ refl)
 
-  surjective : Surjective ≈₂ ≈₁ f⁻¹
-  surjective x = f x , inj (proj₂ (surj (f x)))
+  surjective : Reflexive ≈₁ → Transitive ≈₂ → Surjective ≈₂ ≈₁ f⁻¹
+  surjective refl trans x = f x , inj ∘ trans (f∘f⁻¹≡id _ refl)
 
-  bijective : Symmetric ≈₂ → Transitive ≈₂ → Congruent ≈₁ ≈₂ f → Bijective ≈₂ ≈₁ f⁻¹
-  bijective sym trans cong = injective sym trans cong , surjective
+  bijective : Reflexive ≈₁ → Symmetric ≈₂ → Transitive ≈₂ →
+              Congruent ≈₁ ≈₂ f → Bijective ≈₂ ≈₁ f⁻¹
+  bijective refl sym trans cong = injective refl sym trans cong , surjective refl trans
 
-module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂)
-         (f : A → B) {f⁻¹ : B → A}
-         where
+module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) {f : A → B} {f⁻¹ : B → A} where
 
   inverseʳ : Inverseˡ ≈₁ ≈₂ f f⁻¹ → Inverseʳ ≈₂ ≈₁ f⁻¹ f
   inverseʳ inv = inv
@@ -81,9 +83,9 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂}
         ; isEquivalence₁ = IB.Eq₂.isEquivalence
         ; isEquivalence₂ = IB.Eq₁.isEquivalence
         }
-      ; injective = injective IB.bijective IB.Eq₂.sym IB.Eq₂.trans IB.cong
+      ; injective = injective IB.bijective IB.Eq₁.refl IB.Eq₂.sym IB.Eq₂.trans IB.cong
       }
-    ; surjective = surjective {≈₂ = ≈₂} IB.bijective
+    ; surjective = surjective IB.bijective IB.Eq₁.refl IB.Eq₂.trans
     }
 
 module _ {≈₁ : Rel A ℓ₁} {f : A → B} (isBij : IsBijection ≈₁ _≡_ f) where
@@ -94,35 +96,33 @@ module _ {≈₁ : Rel A ℓ₁} {f : A → B} (isBij : IsBijection ≈₁ _≡_
   isBijection-≡ = isBijection isBij (IB.Eq₁.reflexive ∘ cong _)
     where module IB = IsBijection isBij
 
-module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂}
-         {f : A → B} {f⁻¹ : B → A}
-         where
+module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} {f⁻¹ : B → A} where
 
   isCongruent : IsCongruent ≈₁ ≈₂ f → Congruent ≈₂ ≈₁ f⁻¹ → IsCongruent ≈₂ ≈₁ f⁻¹
   isCongruent ic cg = record
     { cong           = cg
-    ; isEquivalence₁ = IC.isEquivalence₂
-    ; isEquivalence₂ = IC.isEquivalence₁
-    } where module IC = IsCongruent ic
+    ; isEquivalence₁ = F.isEquivalence₂
+    ; isEquivalence₂ = F.isEquivalence₁
+    } where module F = IsCongruent ic
 
   isLeftInverse : IsRightInverse ≈₁ ≈₂ f f⁻¹ → IsLeftInverse ≈₂ ≈₁ f⁻¹ f
   isLeftInverse inv = record
     { isCongruent = isCongruent F.isCongruent F.from-cong
     ; from-cong   = F.cong₁
-    ; inverseˡ    = inverseˡ ≈₁ ≈₂ f {f⁻¹} F.inverseʳ
+    ; inverseˡ    = inverseˡ ≈₁ ≈₂ F.inverseʳ
     } where module F = IsRightInverse inv
 
   isRightInverse : IsLeftInverse ≈₁ ≈₂ f f⁻¹ → IsRightInverse ≈₂ ≈₁ f⁻¹ f
   isRightInverse inv = record
     { isCongruent = isCongruent F.isCongruent F.from-cong
     ; from-cong   = F.to-cong
-    ; inverseʳ    = inverseʳ ≈₁ ≈₂ f {f⁻¹} F.inverseˡ
+    ; inverseʳ    = inverseʳ ≈₁ ≈₂ F.inverseˡ
     } where module F = IsLeftInverse inv
 
   isInverse : IsInverse ≈₁ ≈₂ f f⁻¹ → IsInverse ≈₂ ≈₁ f⁻¹ f
   isInverse f-inv = record
     { isLeftInverse = isLeftInverse F.isRightInverse
-    ; inverseʳ      = inverseʳ ≈₁ ≈₂ f F.inverseˡ
+    ; inverseʳ      = inverseʳ ≈₁ ≈₂ F.inverseˡ
     } where module F = IsInverse f-inv
 
 ------------------------------------------------------------------------
@@ -140,7 +140,7 @@ module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} (bij : Bijection R S) where
   bijection cong = record
     { to        = from
     ; cong      = cong
-    ; bijective = bijective IB.bijective IB.Eq₂.sym IB.Eq₂.trans IB.cong
+    ; bijective = bijective IB.bijective IB.Eq₁.refl IB.Eq₂.sym IB.Eq₂.trans IB.cong
     }
 
 -- We can always flip a bijection if using the equality over the
diff --git a/src/Function/Definitions.agda b/src/Function/Definitions.agda
index bfeff3c05c..225dc53998 100644
--- a/src/Function/Definitions.agda
+++ b/src/Function/Definitions.agda
@@ -8,39 +8,57 @@
 
 {-# 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)
 
-module Function.Definitions
-  {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
+private
+  variable
+    a ℓ₁ ℓ₂ : Level
+    A B : Set a
+
+------------------------------------------------------------------------
+-- Basic definitions
+
+module _
   (_≈₁_ : Rel A ℓ₁) -- Equality over the domain
   (_≈₂_ : Rel B ℓ₂) -- Equality over the codomain
   where
 
-open import Data.Product.Base using (_×_)
-import Function.Definitions.Core1 as Core₁
-import Function.Definitions.Core2 as Core₂
-open import Level using (_⊔_)
+  Congruent : (A → B) → Set _
+  Congruent f = ∀ {x y} → x ≈₁ y → f x ≈₂ f y
 
-------------------------------------------------------------------------
--- Definitions
+  Injective : (A → B) → Set _
+  Injective f = ∀ {x y} → f x ≈₂ f y → x ≈₁ y
 
-Congruent : (A → B) → Set (a ⊔ ℓ₁ ⊔ ℓ₂)
-Congruent f = ∀ {x y} → x ≈₁ y →  f x ≈₂ f y
+  Surjective : (A → B) → Set _
+  Surjective f = ∀ y → ∃ λ x → ∀ {z} → z ≈₁ x → f z ≈₂ y
 
-Injective : (A → B) → Set (a ⊔ ℓ₁ ⊔ ℓ₂)
-Injective f = ∀ {x y} → f x ≈₂ f y → x ≈₁ y
+  Bijective : (A → B) → Set _
+  Bijective f = Injective f × Surjective f
 
-open Core₂ {A = A} _≈₂_ public
-  using (Surjective)
+  Inverseˡ : (A → B) → (B → A) → Set _
+  Inverseˡ f g = ∀ {x y} → y ≈₁ g x → f y ≈₂ x
+
+  Inverseʳ : (A → B) → (B → A) → Set _
+  Inverseʳ f g = ∀ {x y} → y ≈₂ f x → g y ≈₁ x
+
+  Inverseᵇ : (A → B) → (B → A) → Set _
+  Inverseᵇ f g = Inverseˡ f g × Inverseʳ f g
+
+------------------------------------------------------------------------
+-- Strict definitions
 
-Bijective : (A → B) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
-Bijective f = Injective f × Surjective f
+-- These are often easier to use once but much harder to compose and
+-- reason about.
 
-open Core₂ {A = A} _≈₂_ public
-  using (Inverseˡ)
+StrictlySurjective : Rel B ℓ₂ → (A → B) → Set _
+StrictlySurjective _≈₂_ f = ∀ y → ∃ λ x → f x ≈₂ y
 
-open Core₁ {B = B} _≈₁_ public
-  using (Inverseʳ)
+StrictlyInverseˡ : Rel B ℓ₂ → (A → B) → (B → A) → Set _
+StrictlyInverseˡ _≈₂_ f g = ∀ y → f (g y) ≈₂ y
 
-Inverseᵇ : (A → B) → (B → A) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
-Inverseᵇ f g = Inverseˡ f g × Inverseʳ f g
+StrictlyInverseʳ : Rel A ℓ₁ → (A → B) → (B → A) → Set _
+StrictlyInverseʳ _≈₁_ f g = ∀ x → g (f x) ≈₁ x
diff --git a/src/Function/Definitions/Core1.agda b/src/Function/Definitions/Core1.agda
deleted file mode 100644
index b11ca26fea..0000000000
--- a/src/Function/Definitions/Core1.agda
+++ /dev/null
@@ -1,25 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- Definitions for types of functions that only require an equality
--- relation over the domain.
-------------------------------------------------------------------------
-
--- 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.Core1
-  {a b ℓ₁} {A : Set a} {B : Set b} (_≈₁_ : Rel A ℓ₁)
-  where
-
-open import Level using (_⊔_)
-
-------------------------------------------------------------------------
--- Definitions
-
--- (Note the name `RightInverse` is used for the bundle)
-Inverseʳ : (A → B) → (B → A) → Set (a ⊔ ℓ₁)
-Inverseʳ f g = ∀ x → g (f x) ≈₁ x
diff --git a/src/Function/Definitions/Core2.agda b/src/Function/Definitions/Core2.agda
deleted file mode 100644
index 74973d8433..0000000000
--- a/src/Function/Definitions/Core2.agda
+++ /dev/null
@@ -1,29 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- Definitions for types of functions that only require an equality
--- relation over the co-domain.
-------------------------------------------------------------------------
-
--- 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.Core2
-  {a b ℓ₂} {A : Set a} {B : Set b} (_≈₂_ : Rel B ℓ₂)
-  where
-
-open import Data.Product.Base using (∃)
-open import Level using (Level; _⊔_)
-
-------------------------------------------------------------------------
--- Definitions
-
-Surjective : (A → B) → Set (a ⊔ b ⊔ ℓ₂)
-Surjective f = ∀ y → ∃ λ x → f x ≈₂ y
-
--- (Note the name `LeftInverse` is used for the bundle)
-Inverseˡ : (A → B) → (B → A) → Set (b ⊔ ℓ₂)
-Inverseˡ f g = ∀ x → f (g x) ≈₂ x
diff --git a/src/Function/Properties.agda b/src/Function/Properties.agda
index adfb3c73b6..69ae3506c1 100644
--- a/src/Function/Properties.agda
+++ b/src/Function/Properties.agda
@@ -43,6 +43,6 @@ private
 →-cong-↔ extAC extBD A↔B C↔D = mk↔′
   (λ h → C↔D.to   ∘ h ∘ A↔B.from)
   (λ g → C↔D.from ∘ g ∘ A↔B.to  )
-  (λ h → extBD λ x → trans (C↔D.inverseˡ _) (cong h (A↔B.inverseˡ x)))
-  (λ g → extAC λ x → trans (C↔D.inverseʳ _) (cong g (A↔B.inverseʳ x)))
+  (λ h → extBD λ x → trans (C↔D.strictlyInverseˡ _) (cong h (A↔B.strictlyInverseˡ x)))
+  (λ g → extAC λ x → trans (C↔D.strictlyInverseʳ _) (cong g (A↔B.strictlyInverseʳ x)))
   where module A↔B = Inverse A↔B; module C↔D = Inverse C↔D
diff --git a/src/Function/Properties/Bijection.agda b/src/Function/Properties/Bijection.agda
index 89aab1b58e..38d269195b 100644
--- a/src/Function/Properties/Bijection.agda
+++ b/src/Function/Properties/Bijection.agda
@@ -11,10 +11,10 @@ module Function.Properties.Bijection where
 open import Function.Bundles
 open import Level using (Level)
 open import Relation.Binary hiding (_⇔_)
-import Relation.Binary.PropositionalEquality.Properties as P
-import Relation.Binary.Reasoning.Setoid as SetoidReasoning
+open import Relation.Binary.PropositionalEquality as P using (setoid)
 open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Function.Base using (_∘_)
+open import Function.Properties.Surjection using (injective⇒to⁻-cong)
 open import Function.Properties.Inverse using (Inverse⇒Equivalence)
 
 import Function.Construct.Identity as Identity
@@ -55,18 +55,15 @@ trans = Composition.bijection
 -- Conversion functions
 
 Bijection⇒Inverse : Bijection S T → Inverse S T
-Bijection⇒Inverse {S = S} {T = T} b = record
+Bijection⇒Inverse bij = record
   { to        = to
   ; from      = to⁻
   ; to-cong   = cong
-  ; from-cong = λ {x} {y} x≈y → injective (begin
-      to (to⁻ x) ≈⟨ to∘to⁻ x ⟩
-      x          ≈⟨ x≈y ⟩
-      y          ≈˘⟨ to∘to⁻ y ⟩
-      to (to⁻ y) ∎)
-  ; inverse = to∘to⁻ , injective ∘ to∘to⁻ ∘ to
+  ; from-cong = injective⇒to⁻-cong surjection injective
+  ; inverse   = (λ y≈to⁻[x] → Eq₂.trans (cong y≈to⁻[x]) (to∘to⁻ _)) ,
+                (λ y≈to[x] → injective (Eq₂.trans (to∘to⁻ _) y≈to[x]))
   }
-  where open SetoidReasoning T; open Bijection b; to∘to⁻ = proj₂ ∘ surjective
+  where open Bijection bij; to∘to⁻ = proj₂ ∘ strictlySurjective
 
 Bijection⇒Equivalence : Bijection T S → Equivalence T S
 Bijection⇒Equivalence = Inverse⇒Equivalence ∘ Bijection⇒Inverse
diff --git a/src/Function/Properties/Inverse.agda b/src/Function/Properties/Inverse.agda
index 6ef0b45af0..f097945dec 100644
--- a/src/Function/Properties/Inverse.agda
+++ b/src/Function/Properties/Inverse.agda
@@ -57,17 +57,17 @@ open module ↔ {ℓ} = IsEquivalence (↔-isEquivalence {ℓ}) using ()
 -- Conversion functions
 
 Inverse⇒Injection : Inverse S T → Injection S T
-Inverse⇒Injection {S = S} I = record
+Inverse⇒Injection I = record
   { to = to
   ; cong = to-cong
-  ; injective = inverseʳ⇒injective S {f⁻¹ = from} from-cong inverseʳ
+  ; injective = inverseʳ⇒injective Eq₂._≈_ to Eq₂.refl Eq₁.sym Eq₁.trans inverseʳ
   } where open Inverse I
 
 Inverse⇒Bijection : Inverse S T → Bijection S T
-Inverse⇒Bijection {S = S} I = record
+Inverse⇒Bijection I = record
   { to        = to
   ; cong      = to-cong
-  ; bijective = inverseᵇ⇒bijective S from-cong inverse
+  ; bijective = inverseᵇ⇒bijective Eq₂._≈_ Eq₂.refl Eq₁.sym Eq₁.trans inverse
   } where open Inverse I
 
 Inverse⇒Equivalence : Inverse S T → Equivalence S T
@@ -93,6 +93,6 @@ module _ (ext : ∀ {a b} → Extensionality a b) where
   ↔-fun A↔B C↔D = mk↔′
     (λ a→c b → to C↔D (a→c (from A↔B b)))
     (λ b→d a → from C↔D (b→d (to A↔B a)))
-    (λ b→d → ext λ _ → P.trans (inverseˡ C↔D _ ) (P.cong b→d (inverseˡ A↔B _)))
-    (λ a→c → ext λ _ → P.trans (inverseʳ C↔D _ ) (P.cong a→c (inverseʳ A↔B _)))
+    (λ b→d → ext λ _ → P.trans (strictlyInverseˡ C↔D _ ) (P.cong b→d (strictlyInverseˡ A↔B _)))
+    (λ a→c → ext λ _ → P.trans (strictlyInverseʳ C↔D _ ) (P.cong a→c (strictlyInverseʳ A↔B _)))
     where open Inverse
diff --git a/src/Function/Properties/RightInverse.agda b/src/Function/Properties/RightInverse.agda
index f5aa05d9df..66b35e53f0 100644
--- a/src/Function/Properties/RightInverse.agda
+++ b/src/Function/Properties/RightInverse.agda
@@ -10,7 +10,7 @@ module Function.Properties.RightInverse where
 
 open import Function.Base
 open import Function.Bundles
-open import Function.Consequences using (inverseʳ⇒surjective)
+open import Function.Consequences using (inverseˡ⇒surjective)
 open import Level using (Level)
 open import Data.Product
 open import Relation.Binary using (Setoid; IsEquivalence)
@@ -27,7 +27,7 @@ RightInverse⇒Surjection : RightInverse S T → Surjection T S
 RightInverse⇒Surjection I = record
   { to         = from
   ; cong       = from-cong
-  ; surjective = λ a → to a , inverseʳ a
+  ; surjective = inverseˡ⇒surjective Eq₁._≈_ inverseʳ
   } where open RightInverse I
 
 ↪⇒↠ : B ↪ A → A ↠ B
diff --git a/src/Function/Properties/Surjection.agda b/src/Function/Properties/Surjection.agda
index ab164c43d0..fce294be76 100644
--- a/src/Function/Properties/Surjection.agda
+++ b/src/Function/Properties/Surjection.agda
@@ -9,20 +9,39 @@
 module Function.Properties.Surjection where
 
 open import Function.Base
+open import Function.Definitions
 open import Function.Bundles
 open import Level using (Level)
 open import Data.Product
+open import Relation.Binary.PropositionalEquality
+open import Relation.Binary using (Setoid)
+import Relation.Binary.Reasoning.Setoid as SetoidReasoning
 
 private
   variable
-    a b : Level
+    a b ℓ : Level
     A B : Set a
+    T S : Setoid a ℓ
+
+injective⇒to⁻-cong : (surj : Surjection S T) →
+                      (open Surjection surj) →
+                      Injective Eq₁._≈_ Eq₂._≈_ to →
+                      Congruent Eq₂._≈_ Eq₁._≈_ to⁻
+injective⇒to⁻-cong {T = T} surj injective {x} {y} x≈y = injective $ begin
+  to (to⁻ x) ≈⟨ to∘to⁻ x ⟩
+  x          ≈⟨ x≈y ⟩
+  y          ≈˘⟨ to∘to⁻ y ⟩
+  to (to⁻ y) ∎
+  where
+  open SetoidReasoning T
+  open Surjection surj
+  to∘to⁻ = proj₂ ∘ strictlySurjective
 
 ------------------------------------------------------------------------
 -- Conversion functions
 
 ↠⇒↪ : A ↠ B → B ↪ A
-↠⇒↪ s = mk↪ {to = proj₁ ∘ surjective} {from = to} (proj₂ ∘ surjective)
+↠⇒↪ s = mk↪ {from = to} λ { refl → proj₂ (strictlySurjective _)}
   where open Surjection s
 
 ↠⇒⇔ : A ↠ B → A ⇔ B
diff --git a/src/Function/Related.agda b/src/Function/Related.agda
index 12920055af..cc80adff63 100644
--- a/src/Function/Related.agda
+++ b/src/Function/Related.agda
@@ -17,6 +17,7 @@ open import Function.Injection   as Inj     using (Injection; _↣_)
 open import Function.Inverse     as Inv     using (Inverse; _↔_)
 open import Function.LeftInverse as LeftInv using (LeftInverse)
 open import Function.Surjection  as Surj    using (Surjection)
+open import Function.Consequences.Propositional
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as P
@@ -94,12 +95,12 @@ toRelated {K = reverse-implication} rel = lam (B.Func.to rel)
 toRelated {K = equivalence}         rel = Eq.equivalence (B.Equivalence.to rel) (B.Equivalence.from rel)
 toRelated {K = injection}           rel = Inj.injection (B.Injection.to rel) (B.Injection.injective rel)
 toRelated {K = reverse-injection}   rel = lam (Inj.injection (B.Injection.to rel) (B.Injection.injective rel))
-toRelated {K = left-inverse}        rel =
-  LeftInv.leftInverse (B.RightInverse.to rel) (B.RightInverse.from rel) (B.RightInverse.inverseʳ rel)
-toRelated {K = surjection}          rel with B.Surjection.surjective rel
-... | surj = Surj.surjection (B.Surjection.to rel) (proj₁ ∘ surj) (proj₂ ∘ surj)
-toRelated {K = bijection}           rel with B.Bijection.bijective rel
-... | (inj , surj) = Inv.inverse (B.Bijection.to rel) (proj₁ ∘ surj) (inj ∘ proj₂ ∘ surj ∘ (B.Bijection.to rel)) (proj₂ ∘ surj)
+toRelated {K = left-inverse}        rel = LeftInv.leftInverse to from strictlyInverseʳ where open B.RightInverse rel
+toRelated {K = surjection}          rel = Surj.surjection to (proj₁ ∘ strictlySurjective) (proj₂ ∘ strictlySurjective)
+  where open B.Surjection rel
+toRelated {K = bijection}           rel =
+  Inv.inverse to (proj₁ ∘ strictlySurjective) (injective ∘ proj₂ ∘ strictlySurjective ∘ to) (proj₂ ∘ strictlySurjective)
+  where open B.Bijection rel
 
 fromRelated : {K : Kind} → A ∼[ K ] B → A R.∼[ K ] B
 fromRelated {K = implication}         rel = B.mk⟶ rel
@@ -108,13 +109,14 @@ fromRelated {K = equivalence}         record { to = to ; from = from } = B.mk⇔
 fromRelated {K = injection}           rel = B.mk↣ (Inj.Injection.injective rel)
 fromRelated {K = reverse-injection}   (lam app-↢) = B.mk↣ (Inj.Injection.injective app-↢)
 fromRelated {K = left-inverse}        record { to = to ; from = from ; left-inverse-of = left-inverse-of } =
-  B.mk↪ {to = to ⟨$⟩_} {from = from ⟨$⟩_} left-inverse-of
+  B.mk↪ {to = to ⟨$⟩_} {from = from ⟨$⟩_} (strictlyInverseʳ⇒inverseʳ (to ⟨$⟩_) left-inverse-of)
 fromRelated {K = surjection}          record { to = to ; surjective = surjective } with surjective
-... | record { from = from ; right-inverse-of = right-inverse-of } = B.mk↠ {to = to ⟨$⟩_} < from ⟨$⟩_ , right-inverse-of >
+... | record { from = from ; right-inverse-of = right-inverse-of } =
+  B.mk↠ {to = to ⟨$⟩_} < from ⟨$⟩_ , (λ { x P.refl → right-inverse-of x }) >
 fromRelated {K = bijection}           record { to = to ; from = from ; inverse-of = inverse-of } with inverse-of
 ... | record { left-inverse-of = left-inverse-of ; right-inverse-of = right-inverse-of } = B.mk⤖
   ((λ {x y} h → P.subst₂ P._≡_ (left-inverse-of x) (left-inverse-of y) (P.cong (from ⟨$⟩_) h)) ,
-  < from ⟨$⟩_ , right-inverse-of >)
+  < from ⟨$⟩_ , (λ { x P.refl → right-inverse-of x }) >)
 
 -- A non-infix synonym.
 
diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda
index 770dab600e..5566e92c8b 100644
--- a/src/Function/Structures.agda
+++ b/src/Function/Structures.agda
@@ -15,8 +15,10 @@ module Function.Structures {a b ℓ₁ ℓ₂}
   {B : Set b} (_≈₂_ : Rel B ℓ₂) -- Equality over the codomain
   where
 
-open import Data.Product.Base using (_,_)
+open import Data.Product.Base as Product using (∃; _×_; _,_)
+open import Function.Base
 open import Function.Definitions
+open import Function.Consequences
 open import Level using (_⊔_)
 
 ------------------------------------------------------------------------
@@ -63,6 +65,9 @@ record IsSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
 
   open IsCongruent isCongruent public
 
+  strictlySurjective : StrictlySurjective _≈₂_ f
+  strictlySurjective x = Product.map₂ (λ v → v Eq₁.refl) (surjective x)
+
 
 record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
   field
@@ -80,6 +85,9 @@ record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
     ; surjective  = surjective
     }
 
+  open IsSurjection isSurjection public
+    using (strictlySurjective)
+
 
 ------------------------------------------------------------------------
 -- Two element structures
@@ -94,6 +102,9 @@ record IsLeftInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ 
   open IsCongruent isCongruent public
     renaming (cong to to-cong)
 
+  strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to from
+  strictlyInverseˡ x = inverseˡ Eq₁.refl
+
 
 record IsRightInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
   field
@@ -104,6 +115,9 @@ record IsRightInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁
   open IsCongruent isCongruent public
     renaming (cong to cong₁)
 
+  strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to from
+  strictlyInverseʳ x = inverseʳ Eq₂.refl
+
 
 record IsInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
   field
@@ -119,6 +133,9 @@ record IsInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ 
     ; inverseʳ    = inverseʳ
     }
 
+  open IsRightInverse isRightInverse public
+    using (strictlyInverseʳ)
+
   inverse : Inverseᵇ _≈₁_ _≈₂_ to from
   inverse = inverseˡ , inverseʳ
 
diff --git a/src/Relation/Binary/Morphism/Construct/Composition.agda b/src/Relation/Binary/Morphism/Construct/Composition.agda
index 202605b608..5f6fe9bf32 100644
--- a/src/Relation/Binary/Morphism/Construct/Composition.agda
+++ b/src/Relation/Binary/Morphism/Construct/Composition.agda
@@ -46,9 +46,9 @@ isRelIsomorphism : Transitive ≈₃ →
                    IsRelIsomorphism ≈₁ ≈₂ f →
                    IsRelIsomorphism ≈₂ ≈₃ g →
                    IsRelIsomorphism ≈₁ ≈₃ (g ∘ f)
-isRelIsomorphism {≈₁ = ≈₁} ≈₃-trans m₁ m₂ = record
+isRelIsomorphism  {≈₃ = ≈₃} ≈₃-trans m₁ m₂ = record
   { isMonomorphism = isRelMonomorphism F.isMonomorphism G.isMonomorphism
-  ; surjective     = surjective ≈₁ _ _ ≈₃-trans G.cong F.surjective G.surjective
+  ; surjective     = surjective _ _ ≈₃ F.surjective G.surjective
   } where module F = IsRelIsomorphism m₁; module G = IsRelIsomorphism m₂
 
 ------------------------------------------------------------------------
@@ -103,9 +103,9 @@ isOrderIsomorphism : Transitive ≈₃ →
                      IsOrderIsomorphism ≈₁ ≈₂ ∼₁ ∼₂ f →
                      IsOrderIsomorphism ≈₂ ≈₃ ∼₂ ∼₃ g →
                      IsOrderIsomorphism ≈₁ ≈₃ ∼₁ ∼₃ (g ∘ f)
-isOrderIsomorphism {≈₁ = ≈₁} ≈₃-trans m₁ m₂ = record
+isOrderIsomorphism {≈₃ = ≈₃}  ≈₃-trans m₁ m₂ = record
   { isOrderMonomorphism = isOrderMonomorphism F.isOrderMonomorphism G.isOrderMonomorphism
-  ; surjective          = surjective ≈₁ _ _ ≈₃-trans G.cong F.surjective G.surjective
+  ; surjective          = surjective _ _ ≈₃ F.surjective G.surjective
   } where module F = IsOrderIsomorphism m₁; module G = IsOrderIsomorphism m₂
 
 ------------------------------------------------------------------------
diff --git a/src/Relation/Binary/Morphism/Construct/Identity.agda b/src/Relation/Binary/Morphism/Construct/Identity.agda
index db12c9793b..302881b4aa 100644
--- a/src/Relation/Binary/Morphism/Construct/Identity.agda
+++ b/src/Relation/Binary/Morphism/Construct/Identity.agda
@@ -8,6 +8,7 @@
 
 open import Data.Product.Base using (_,_)
 open import Function.Base using (id)
+import Function.Construct.Identity as Id
 open import Level using (Level)
 open import Relation.Binary
 open import Relation.Binary.Morphism.Structures
@@ -29,19 +30,19 @@ module _ (≈ : Rel A ℓ₁) where
 
   isRelHomomorphism : IsRelHomomorphism ≈ ≈ id
   isRelHomomorphism = record
-    { cong = id
+    { cong = Id.congruent ≈
     }
 
   isRelMonomorphism : IsRelMonomorphism ≈ ≈ id
   isRelMonomorphism = record
     { isHomomorphism = isRelHomomorphism
-    ; injective      = id
+    ; injective      = Id.injective ≈
     }
 
   isRelIsomorphism : Reflexive ≈ → IsRelIsomorphism ≈ ≈ id
   isRelIsomorphism refl = record
     { isMonomorphism = isRelMonomorphism
-    ; surjective     = λ y → y , refl
+    ; surjective     = Id.surjective ≈
     }
 
 ------------------------------------------------------------------------
@@ -76,14 +77,14 @@ module _ (≈ : Rel A ℓ₁) (∼ : Rel A ℓ₂) where
   isOrderMonomorphism : IsOrderMonomorphism ≈ ≈ ∼ ∼ id
   isOrderMonomorphism = record
     { isOrderHomomorphism = isOrderHomomorphism
-    ; injective           = id
+    ; injective           = Id.injective ≈
     ; cancel              = id
     }
 
   isOrderIsomorphism : Reflexive ≈ → IsOrderIsomorphism ≈ ≈ ∼ ∼ id
   isOrderIsomorphism refl = record
     { isOrderMonomorphism = isOrderMonomorphism
-    ; surjective          = λ y → y , refl
+    ; surjective          = Id.surjective ≈
     }
 
 ------------------------------------------------------------------------