diff --git a/CHANGELOG.md b/CHANGELOG.md
index c8ccab3fb9..d610fc8de6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -17,6 +17,19 @@ Bug-fixes
   the record constructors `_,_` incorrectly had no declared fixity. They have been given
   the fixity `infixr 4 _,_`, consistent with that of `Data.Product.Base`.
 
+* A major overhaul of the `Function` hierarchy sees the systematic development
+  and use of the theory of the left inverse `from` to a given `Surjective` function
+  `to`, as a consequence of which we can achieve full symmetry of `Bijection`, in
+  `Function.Properties.Bijection`/`Function.Construct.Symmetry`, rather than the
+  restricted versions considered to date. NB. this is non-backwards compatible
+  because the types of various properties are now sharper, and some previous lemmas
+  are no longer present, due to the complexity their deprecation would entail.
+  Specifically:
+  - `Function.Construct.Symmetry.isBijection` no longer requires the hypothesis `Congruent ≈₂ ≈₁ f⁻¹` for the function `f⁻¹ = B.from`.
+  - `Function.Construct.Symmetry.isBijection-≡` is now redundant, as an instance of the above lemma, so has been deleted.
+  - Similarly, `Function.Construct.Symmetry.bijection` no longer requires a `Congruent` hypothesis, and `Function.Construct.Symmetry.bijection-≡` is now redundant/deleted.
+  - `Function.Properties.Bijection.sym-≡` is now redundant as an instance of a fully general symmetry property `Function.Properties.Bijection.sym`, hence also deleted.
+
 Non-backwards compatible changes
 --------------------------------
 
@@ -28,6 +41,8 @@ Non-backwards compatible changes
 Minor improvements
 ------------------
 
+* The definitions in `Function.Consequences.Propositional` of the form `strictlyX⇒X` have been streamlined via pattern-matching on `refl`, rather than defined by delegation to `Function.Consequences.Setoid` and the use of `cong`.
+
 * Moved the concept `Irrelevant` of irrelevance (h-proposition) from `Relation.Nullary`
   to its own dedicated module `Relation.Nullary.Irrelevant`.
 
@@ -116,6 +131,17 @@ Deprecated names
   product-↭   ↦  Data.Nat.ListAction.Properties.product-↭
   ```
 
+* In `Function.Bundles.IsSurjection`:
+  ```agda
+  to⁻      ↦  Function.Structures.IsSurjection.from
+  to∘to⁻   ↦  Function.Structures.IsSurjection.strictlyInverseˡ
+  ```
+
+* In `Function.Properties.Surjection`:
+  ```agda
+  injective⇒to⁻-cong   ↦  Function.Bundles.Bijection.from-cong
+  ```
+
 New modules
 -----------
 
@@ -206,6 +232,78 @@ Additions to existing modules
   filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys
   ```
 
+* In `Function.Bundles.Bijection`:
+  ```agda
+  from             : B → A
+  inverseˡ         : Inverseˡ _≈₁_ _≈₂_ to from
+  strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to from
+  inverseʳ         : Inverseʳ _≈₁_ _≈₂_ to from
+  strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to from
+  ```
+
+* In `Function.Bundles.LeftInverse`:
+  ```agda
+  surjective       : Surjective _≈₁_ _≈₂_ to
+  surjection       : Surjection From To
+  ```
+
+* In `Function.Bundles.RightInverse`:
+  ```agda
+  isInjection      : IsInjection to
+  injective        : Injective _≈₁_ _≈₂_ to
+  injection        : Injection From To
+  ```
+
+* In `Function.Bundles.Surjection`:
+  ```agda
+  from             : B → A
+  inverseˡ         : Inverseˡ _≈₁_ _≈₂_ to from
+  strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to from
+  ```
+
+* In `Function.Construct.Symmetry`:
+  ```agda
+  isBijection : IsBijection ≈₁ ≈₂ to → IsBijection ≈₂ ≈₁ from
+  bijection   : Bijection R S → Bijection S R
+  ```
+
+* In `Function.Properties.Bijection`:
+  ```agda
+  sym : Bijection S T → Bijection T S
+  ```
+
+* In `Function.Structures.IsBijection`:
+  ```agda
+  from             : B → A
+  inverseˡ         : Inverseˡ _≈₁_ _≈₂_ to from
+  strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to from
+  inverseʳ         : Inverseʳ _≈₁_ _≈₂_ to from
+  strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to from
+  from-cong        : Congruent _≈₂_ _≈₁_ from
+  from-injective   : Injective _≈₂_ _≈₁_ from
+  from-surjective  : Surjective _≈₂_ _≈₁_ from
+  from-bijective   : Bijective _≈₂_ _≈₁_ from
+  ```
+
+* In `Function.Structures.IsLeftInverse`:
+  ```agda
+  surjective : Surjective _≈₁_ _≈₂_ to
+  ```
+
+* In `Function.Structures.IsRightInverse`:
+  ```agda
+  injective   : Injective _≈₁_ _≈₂_ to
+  isInjection : IsInjection to
+  ```
+
+* In `Function.Structures.IsSurjection`:
+  ```agda
+  from             : B → A
+  inverseˡ         : Inverseˡ _≈₁_ _≈₂_ to from
+  strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to from
+  from-injective   : Injective _≈₂_ _≈₁_ from
+  ```
+
 * In `Relation.Binary.Construct.Add.Infimum.Strict`:
   ```agda
   <₋-accessible-⊥₋ : Acc _<₋_ ⊥₋
diff --git a/src/Data/Product/Function/Dependent/Propositional.agda b/src/Data/Product/Function/Dependent/Propositional.agda
index 4c6f391e2f..ba9db6fb6e 100644
--- a/src/Data/Product/Function/Dependent/Propositional.agda
+++ b/src/Data/Product/Function/Dependent/Propositional.agda
@@ -57,7 +57,7 @@ module _ where
          Σ I A ⇔ Σ J B
   Σ-⇔ {B = B} I↠J A⇔B = mk⇔
     (map (to  I↠J) (Equivalence.to A⇔B))
-    (map (to⁻ I↠J) (Equivalence.from A⇔B ∘ ≡.subst B (≡.sym (proj₂ (surjective I↠J _) ≡.refl))))
+    (map (from I↠J) (Equivalence.from A⇔B ∘ ≡.subst B (≡.sym (proj₂ (surjective I↠J _) ≡.refl))))
 
   -- See also Data.Product.Relation.Binary.Pointwise.Dependent.WithK.↣.
 
@@ -193,18 +193,22 @@ module _ where
     to′ : Σ I A → Σ J B
     to′ = map (to I↠J) (to A↠B)
 
-    backcast : ∀ {i} → B i → B (to I↠J (to⁻ I↠J i))
-    backcast = ≡.subst B (≡.sym (to∘to⁻ I↠J _))
+    backcast : ∀ {i} → B i → B (to I↠J (from I↠J i))
+    backcast = ≡.subst B (≡.sym (strictlyInverseˡ I↠J _))
 
-    to⁻′ : Σ J B → Σ I A
-    to⁻′ = map (to⁻ I↠J) (Surjection.to⁻ A↠B ∘ backcast)
+    from′ : Σ J B → Σ I A
+    from′ = map (from I↠J) (from A↠B ∘ backcast)
 
     strictlySurjective′ : StrictlySurjective _≡_ to′
-    strictlySurjective′ (x , y) = to⁻′ (x , y) , Σ-≡,≡→≡
-      ( to∘to⁻ I↠J x
-      , (≡.subst B (to∘to⁻ I↠J x) (to A↠B (to⁻ A↠B (backcast y))) ≡⟨ ≡.cong (≡.subst B _) (to∘to⁻ A↠B _) ⟩
-         ≡.subst B (to∘to⁻ I↠J x) (backcast y)                      ≡⟨ ≡.subst-subst-sym (to∘to⁻ I↠J x) ⟩
-         y                                                          ∎)
+    strictlySurjective′ (x , y) = from′ (x , y) , Σ-≡,≡→≡
+      ( strictlyInverseˡ I↠J x
+      , (begin
+           ≡.subst B (strictlyInverseˡ I↠J x) (to A↠B (from A↠B (backcast y)))
+             ≡⟨ ≡.cong (≡.subst B _) (strictlyInverseˡ A↠B _) ⟩
+           ≡.subst B (strictlyInverseˡ I↠J x) (backcast y)
+             ≡⟨ ≡.subst-subst-sym (strictlyInverseˡ I↠J x) ⟩
+           y
+             ∎)
       ) where open ≡.≡-Reasoning
 
 
@@ -249,8 +253,8 @@ module _ where
       Σ I A ↔ Σ J B
   Σ-↔ {I = I} {J = J} {A = A} {B = B} I↔J A↔B = mk↔ₛ′
     (Surjection.to surjection′)
-    (Surjection.to⁻ surjection′)
-    (Surjection.to∘to⁻ surjection′)
+    (Surjection.from surjection′)
+    (Surjection.strictlyInverseˡ surjection′)
     left-inverse-of
     where
     open ≡.≡-Reasoning
@@ -260,7 +264,7 @@ module _ where
     surjection′ : Σ I A ↠ Σ J B
     surjection′ = Σ-↠ (↔⇒↠ (≃⇒↔ I≃J)) (↔⇒↠ A↔B)
 
-    left-inverse-of : ∀ p → Surjection.to⁻ surjection′ (Surjection.to surjection′ p) ≡ p
+    left-inverse-of : ∀ p → Surjection.from surjection′ (Surjection.to surjection′ p) ≡ p
     left-inverse-of (x , y) = to Σ-≡,≡↔≡
       ( _≃_.left-inverse-of I≃J x
       , (≡.subst A (_≃_.left-inverse-of I≃J x)
diff --git a/src/Data/Product/Function/Dependent/Setoid.agda b/src/Data/Product/Function/Dependent/Setoid.agda
index 0ad3785ed7..671b219a54 100644
--- a/src/Data/Product/Function/Dependent/Setoid.agda
+++ b/src/Data/Product/Function/Dependent/Setoid.agda
@@ -94,34 +94,37 @@ module _ where
     (function (⇔⇒⟶ I⇔J) A⟶B)
     (function (⇔⇒⟵ I⇔J) B⟶A)
 
-  equivalence-↪ :
-    (I↪J : I ↪ J) →
-    (∀ {i} → Equivalence (A atₛ (RightInverse.from I↪J i)) (B atₛ i)) →
-    Equivalence (I ×ₛ A) (J ×ₛ B)
-  equivalence-↪ {A = A} {B = B} I↪J A⇔B =
-    equivalence (RightInverse.equivalence I↪J) A→B (fromFunction A⇔B)
-    where
-    A→B : ∀ {i} → Func (A atₛ i) (B atₛ (RightInverse.to I↪J i))
-    A→B = record
-      { to   = to      A⇔B ∘ cast      A (RightInverse.strictlyInverseʳ I↪J _)
-      ; cong = to-cong A⇔B ∘ cast-cong A (RightInverse.strictlyInverseʳ I↪J _)
-      }
+  module _ (I↪J : I ↪ J) where
 
-  equivalence-↠ :
-    (I↠J : I ↠ J) →
-    (∀ {x} → Equivalence (A atₛ x) (B atₛ (Surjection.to I↠J x))) →
-    Equivalence (I ×ₛ A) (J ×ₛ B)
-  equivalence-↠ {A = A} {B = B} I↠J A⇔B =
-    equivalence (↠⇒⇔ I↠J) B-to B-from
-    where
-    B-to : ∀ {x} → Func (A atₛ x) (B atₛ (Surjection.to I↠J x))
-    B-to = toFunction A⇔B
+    private module ItoJ = RightInverse I↪J
 
-    B-from : ∀ {y} → Func (B atₛ y) (A atₛ (Surjection.to⁻ I↠J y))
-    B-from = record
-      { to   = from      A⇔B ∘ cast      B (Surjection.to∘to⁻ I↠J _)
-      ; cong = from-cong A⇔B ∘ cast-cong B (Surjection.to∘to⁻ I↠J _)
-      }
+    equivalence-↪ : (∀ {i} → Equivalence (A atₛ (ItoJ.from i)) (B atₛ i)) →
+                    Equivalence (I ×ₛ A) (J ×ₛ B)
+    equivalence-↪ {A = A} {B = B} A⇔B =
+      equivalence ItoJ.equivalence A→B (fromFunction A⇔B)
+      where
+      A→B : ∀ {i} → Func (A atₛ i) (B atₛ (ItoJ.to i))
+      A→B = record
+        { to   = to      A⇔B ∘ cast      A (ItoJ.strictlyInverseʳ _)
+        ; cong = to-cong A⇔B ∘ cast-cong A (ItoJ.strictlyInverseʳ _)
+        }
+
+  module _ (I↠J : I ↠ J) where
+
+    private module ItoJ = Surjection I↠J
+
+    equivalence-↠ : (∀ {x} → Equivalence (A atₛ x) (B atₛ (ItoJ.to x))) →
+                    Equivalence (I ×ₛ A) (J ×ₛ B)
+    equivalence-↠ {A = A} {B = B} A⇔B = equivalence (↠⇒⇔ I↠J) B-to B-from
+      where
+      B-to : ∀ {x} → Func (A atₛ x) (B atₛ (ItoJ.to x))
+      B-to = toFunction A⇔B
+
+      B-from : ∀ {y} → Func (B atₛ y) (A atₛ (ItoJ.from y))
+      B-from = record
+        { to   = from      A⇔B ∘ cast      B (ItoJ.strictlyInverseˡ _)
+        ; cong = from-cong A⇔B ∘ cast-cong B (ItoJ.strictlyInverseˡ _)
+        }
 
 ------------------------------------------------------------------------
 -- Injections
@@ -168,12 +171,12 @@ module _ where
     func : Func (I ×ₛ A) (J ×ₛ B)
     func = function (Surjection.function I↠J) (Surjection.function A↠B)
 
-    to⁻′ : Carrier (J ×ₛ B) → Carrier (I ×ₛ A)
-    to⁻′ (j , y) = to⁻ I↠J j , to⁻ A↠B (cast B (Surjection.to∘to⁻ I↠J _) y)
+    from′ : Carrier (J ×ₛ B) → Carrier (I ×ₛ A)
+    from′ (j , y) = from I↠J j , from A↠B (cast B (strictlyInverseˡ I↠J _) y)
 
     strictlySurj : StrictlySurjective (Func.Eq₂._≈_ func) (Func.to func)
-    strictlySurj (j , y) = to⁻′ (j , y) ,
-      to∘to⁻ I↠J j , IndexedSetoid.trans B (to∘to⁻ A↠B _) (cast-eq B (to∘to⁻ I↠J j))
+    strictlySurj (j , y) = from′ (j , y) ,
+      strictlyInverseˡ I↠J j , IndexedSetoid.trans B (strictlyInverseˡ A↠B _) (cast-eq B (strictlyInverseˡ I↠J j))
 
     surj : Surjective (Func.Eq₁._≈_ func) (Func.Eq₂._≈_ func) (Func.to func)
     surj = strictlySurjective⇒surjective (I ×ₛ A) (J ×ₛ B) (Func.cong func) strictlySurj
diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda
index 9667e33cc6..e2c8298dc6 100644
--- a/src/Function/Bundles.agda
+++ b/src/Function/Bundles.agda
@@ -20,15 +20,15 @@
 module Function.Bundles where
 
 open import Function.Base using (_∘_)
+open import Function.Consequences.Propositional
+  using (strictlySurjective⇒surjective; strictlyInverseˡ⇒inverseˡ; strictlyInverseʳ⇒inverseʳ)
 open import Function.Definitions
 import Function.Structures as FunctionStructures
 open import Level using (Level; _⊔_; suc)
 open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.Core using (_Preserves_⟶_)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as ≡
-open import Function.Consequences.Propositional
 open Setoid using (isEquivalence)
 
 private
@@ -112,13 +112,24 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
     open IsSurjection isSurjection public
       using
       ( strictlySurjective
+      ; from
+      ; inverseˡ
+      ; strictlyInverseˡ
       )
 
     to⁻ : B → A
-    to⁻ = proj₁ ∘ surjective
+    to⁻ = from
+    {-# WARNING_ON_USAGE to⁻
+    "Warning: to⁻ was deprecated in v2.3.
+    Please use Function.Structures.IsSurjection.from instead. "
+    #-}
 
-    to∘to⁻ : ∀ x → to (to⁻ x) ≈₂ x
-    to∘to⁻ = proj₂ ∘ strictlySurjective
+    to∘to⁻ : StrictlyInverseˡ _≈₂_ to from
+    to∘to⁻ = strictlyInverseˡ
+    {-# WARNING_ON_USAGE to∘to⁻
+    "Warning: to∘to⁻ was deprecated in v2.3.
+    Please use Function.Structures.IsSurjection.strictlyInverseˡ instead. "
+    #-}
 
 
   record Bijection : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
@@ -145,8 +156,15 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
       ; surjective = surjective
       }
 
-    open Injection  injection  public using (isInjection)
-    open Surjection surjection public using (isSurjection; to⁻;  strictlySurjective)
+    open Injection  injection  public
+      using (isInjection)
+    open Surjection surjection public
+      using (isSurjection
+            ; strictlySurjective
+            ; from
+            ; inverseˡ
+            ; strictlyInverseˡ
+            )
 
     isBijection : IsBijection to
     isBijection = record
@@ -154,7 +172,11 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
       ; surjective  = surjective
       }
 
-    open IsBijection isBijection public using (module Eq₁; module Eq₂)
+    open IsBijection isBijection public
+      using (module Eq₁; module Eq₂
+            ; inverseʳ; strictlyInverseʳ
+            ; from-cong; from-injective; from-surjective; from-bijective
+            )
 
 
 ------------------------------------------------------------------------
@@ -219,6 +241,8 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
     open IsLeftInverse isLeftInverse public
       using (module Eq₁; module Eq₂; strictlyInverseˡ; isSurjection)
 
+    open IsSurjection isSurjection public using (surjective)
+
     equivalence : Equivalence
     equivalence = record
       { to-cong   = to-cong
@@ -235,7 +259,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
     surjection = record
       { to = to
       ; cong = to-cong
-      ; surjective = λ y → from y , inverseˡ
+      ; surjective = surjective
       }
 
 
@@ -245,7 +269,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
       to        : A → B
       from      : B → A
       to-cong   : Congruent _≈₁_ _≈₂_ to
-      from-cong : from Preserves _≈₂_ ⟶ _≈₁_
+      from-cong : Congruent _≈₂_ _≈₁_ from
       inverseʳ  : Inverseʳ _≈₁_ _≈₂_ to from
 
     isCongruent : IsCongruent to
@@ -263,7 +287,9 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
       }
 
     open IsRightInverse isRightInverse public
-      using (module Eq₁; module Eq₂; strictlyInverseʳ)
+      using (module Eq₁; module Eq₂; strictlyInverseʳ; isInjection)
+
+    open IsInjection isInjection public using (injective)
 
     equivalence : Equivalence
     equivalence = record
@@ -271,6 +297,13 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
       ; from-cong = from-cong
       }
 
+    injection : Injection From To
+    injection = record
+      { to = to
+      ; cong = to-cong
+      ; injective = injective
+      }
+
 
   record Inverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
     field
@@ -369,7 +402,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
   -- function for elements `x₁` and `x₂` are equal if `x₁ ≈ x₂` .
   --
   -- The difference is the `from-cong` law --- generally, the section
-  -- (called `Surjection.to⁻` or `SplitSurjection.from`) of a surjection
+  -- (called `Surjection.from` or `SplitSurjection.from`) of a surjection
   -- need not respect equality, whereas it must in a split surjection.
   --
   -- The two notions coincide when the equivalence relation on `B` is
diff --git a/src/Function/Consequences.agda b/src/Function/Consequences.agda
index 2a13d452f6..d908f536f8 100644
--- a/src/Function/Consequences.agda
+++ b/src/Function/Consequences.agda
@@ -11,6 +11,7 @@
 module Function.Consequences where
 
 open import Data.Product.Base as Product
+open import Function.Base using (_∘_)
 open import Function.Definitions
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
@@ -23,14 +24,15 @@ private
     a b ℓ₁ ℓ₂ : Level
     A B : Set a
     ≈₁ ≈₂ : Rel A ℓ₁
-    f f⁻¹ : A → B
+    f : A → B
+    f⁻¹ : B → A
 
 ------------------------------------------------------------------------
 -- Injective
 
 contraInjective : ∀ (≈₂ : Rel B ℓ₂) → Injective ≈₁ ≈₂ f →
                   ∀ {x y} → ¬ (≈₁ x y) → ¬ (≈₂ (f x) (f y))
-contraInjective _ inj p = contraposition inj p
+contraInjective _ inj = contraposition inj
 
 ------------------------------------------------------------------------
 -- Inverseˡ
@@ -38,7 +40,7 @@ contraInjective _ inj p = contraposition inj p
 inverseˡ⇒surjective : ∀ (≈₂ : Rel B ℓ₂) →
                       Inverseˡ ≈₁ ≈₂ f f⁻¹ →
                       Surjective ≈₁ ≈₂ f
-inverseˡ⇒surjective ≈₂ invˡ y = (_ , invˡ)
+inverseˡ⇒surjective ≈₂ invˡ _ = (_ , invˡ)
 
 ------------------------------------------------------------------------
 -- Inverseʳ
@@ -49,8 +51,7 @@ inverseʳ⇒injective : ∀ (≈₂ : Rel B ℓ₂) f →
                      Transitive ≈₁ →
                      Inverseʳ ≈₁ ≈₂ f f⁻¹ →
                      Injective ≈₁ ≈₂ f
-inverseʳ⇒injective ≈₂ f refl sym trans invʳ {x} {y} fx≈fy =
-  trans (sym (invʳ refl)) (invʳ fx≈fy)
+inverseʳ⇒injective ≈₂ f refl sym trans invʳ = trans (sym (invʳ refl)) ∘ invʳ
 
 ------------------------------------------------------------------------
 -- Inverseᵇ
@@ -71,8 +72,7 @@ surjective⇒strictlySurjective : ∀ (≈₂ : Rel B ℓ₂) →
                                  Reflexive ≈₁ →
                                  Surjective ≈₁ ≈₂ f →
                                  StrictlySurjective ≈₂ f
-surjective⇒strictlySurjective _ refl surj x =
-  Product.map₂ (λ v → v refl) (surj x)
+surjective⇒strictlySurjective _ refl surj = Product.map₂ (λ v → v refl) ∘ surj
 
 strictlySurjective⇒surjective : Transitive ≈₂ →
                                  Congruent ≈₁ ≈₂ f →
@@ -104,11 +104,13 @@ inverseʳ⇒strictlyInverseʳ : ∀ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ
                             Reflexive ≈₂ →
                             Inverseʳ ≈₁ ≈₂ f f⁻¹ →
                             StrictlyInverseʳ ≈₁ f f⁻¹
-inverseʳ⇒strictlyInverseʳ _ _ refl sinv x = sinv refl
+inverseʳ⇒strictlyInverseʳ  {f = f} {f⁻¹ = f⁻¹} ≈₁ ≈₂ =
+  inverseˡ⇒strictlyInverseˡ {f = f⁻¹} {f⁻¹ = f} ≈₂ ≈₁
 
 strictlyInverseʳ⇒inverseʳ : Transitive ≈₁ →
                             Congruent ≈₂ ≈₁ f⁻¹ →
                             StrictlyInverseʳ ≈₁ f f⁻¹ →
                             Inverseʳ ≈₁ ≈₂ f f⁻¹
-strictlyInverseʳ⇒inverseʳ trans cong sinv {x} y≈f⁻¹x =
-  trans (cong y≈f⁻¹x) (sinv x)
+strictlyInverseʳ⇒inverseʳ {≈₁ = ≈₁} {≈₂ = ≈₂} {f⁻¹ = f⁻¹} {f = f} =
+  strictlyInverseˡ⇒inverseˡ {≈₂ = ≈₁} {≈₁ = ≈₂} {f = f⁻¹} {f⁻¹ = f}
+
diff --git a/src/Function/Consequences/Propositional.agda b/src/Function/Consequences/Propositional.agda
index 80b4556e42..24aa4b7b02 100644
--- a/src/Function/Consequences/Propositional.agda
+++ b/src/Function/Consequences/Propositional.agda
@@ -11,20 +11,19 @@ module Function.Consequences.Propositional
   {a b} {A : Set a} {B : Set b}
   where
 
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; cong)
+open import Data.Product.Base using (_,_)
+open import Function.Definitions
+  using (StrictlySurjective; StrictlyInverseˡ; StrictlyInverseʳ
+        ; Surjective; Inverseˡ; Inverseʳ)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Relation.Binary.PropositionalEquality.Properties
   using (setoid)
-open import Function.Definitions
-  using (StrictlySurjective; StrictlyInverseˡ; StrictlyInverseʳ; Inverseˡ
-        ; Inverseʳ; Surjective)
-open import Relation.Nullary.Negation.Core using (contraposition)
 
-import Function.Consequences.Setoid (setoid A) (setoid B) as Setoid
 
 ------------------------------------------------------------------------
 -- Re-export setoid properties
 
-open Setoid public
+open import Function.Consequences.Setoid (setoid A) (setoid B) public
   hiding
   ( strictlySurjective⇒surjective
   ; strictlyInverseˡ⇒inverseˡ
@@ -41,15 +40,14 @@ private
 
 strictlySurjective⇒surjective : StrictlySurjective _≡_ f →
                                  Surjective _≡_ _≡_ f
-strictlySurjective⇒surjective =
- Setoid.strictlySurjective⇒surjective (cong _)
+strictlySurjective⇒surjective surj y =
+  let x , fx≡y = surj y in x , λ where refl → fx≡y
 
 strictlyInverseˡ⇒inverseˡ : ∀ f → StrictlyInverseˡ _≡_ f f⁻¹ →
                             Inverseˡ _≡_ _≡_ f f⁻¹
-strictlyInverseˡ⇒inverseˡ f =
-  Setoid.strictlyInverseˡ⇒inverseˡ (cong _)
+strictlyInverseˡ⇒inverseˡ _ inv refl = inv _
 
 strictlyInverseʳ⇒inverseʳ : ∀ f → StrictlyInverseʳ _≡_ f f⁻¹ →
                             Inverseʳ _≡_ _≡_ f f⁻¹
-strictlyInverseʳ⇒inverseʳ f =
-  Setoid.strictlyInverseʳ⇒inverseʳ (cong _)
+strictlyInverseʳ⇒inverseʳ _ inv refl = inv _
+
diff --git a/src/Function/Construct/Symmetry.agda b/src/Function/Construct/Symmetry.agda
index e9bf2d8cd7..552e84f9a1 100644
--- a/src/Function/Construct/Symmetry.agda
+++ b/src/Function/Construct/Symmetry.agda
@@ -8,8 +8,8 @@
 
 module Function.Construct.Symmetry where
 
-open import Data.Product.Base using (_,_; swap; proj₁; proj₂)
-open import Function.Base using (_∘_)
+open import Data.Product.Base using (_,_; swap)
+open import Function.Base using (_∘_; id)
 open import Function.Definitions
   using (Bijective; Injective; Surjective; Inverseˡ; Inverseʳ; Inverseᵇ
         ; Congruent)
@@ -22,7 +22,7 @@ open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive)
 open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 open import Relation.Binary.PropositionalEquality.Properties using (setoid)
 
 private
@@ -33,71 +33,39 @@ private
 ------------------------------------------------------------------------
 -- Properties
 
-module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B}
-         ((inj , surj) : Bijective ≈₁ ≈₂ f)
-         where
-
-  private
-    f⁻¹      = proj₁ ∘ surj
-    f∘f⁻¹≡id = proj₂ ∘ surj
-
-  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 : Reflexive ≈₁ → Transitive ≈₂ → Surjective ≈₂ ≈₁ f⁻¹
-  surjective refl trans x = f x , inj ∘ trans (f∘f⁻¹≡id _ refl)
-
-  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
 
   inverseʳ : Inverseˡ ≈₁ ≈₂ f f⁻¹ → Inverseʳ ≈₂ ≈₁ f⁻¹ f
-  inverseʳ inv = inv
+  inverseʳ = id
 
   inverseˡ : Inverseʳ ≈₁ ≈₂ f f⁻¹ → Inverseˡ ≈₂ ≈₁ f⁻¹ f
-  inverseˡ inv = inv
+  inverseˡ = id
 
   inverseᵇ : Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Inverseᵇ ≈₂ ≈₁ f⁻¹ f
-  inverseᵇ (invˡ , invʳ) = (invʳ , invˡ)
+  inverseᵇ = swap
 
 ------------------------------------------------------------------------
 -- Structures
 
-module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂}
-         {f : A → B} (isBij : IsBijection ≈₁ ≈₂ f)
+module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {to : A → B}
+         (isBij : IsBijection ≈₁ ≈₂ to)
          where
 
-  private
-    module IB = IsBijection isBij
-    f⁻¹       = proj₁ ∘ IB.surjective
+  private module B = IsBijection isBij
 
-  -- We can only flip a bijection if the witness produced by the
-  -- surjection proof respects the equality on the codomain.
-  isBijection : Congruent ≈₂ ≈₁ f⁻¹ → IsBijection ≈₂ ≈₁ f⁻¹
-  isBijection f⁻¹-cong = record
+  isBijection : IsBijection ≈₂ ≈₁ B.from
+  isBijection = record
     { isInjection = record
       { isCongruent = record
-        { cong           = f⁻¹-cong
-        ; isEquivalence₁ = IB.Eq₂.isEquivalence
-        ; isEquivalence₂ = IB.Eq₁.isEquivalence
+        { cong           = B.from-cong
+        ; isEquivalence₁ = B.Eq₂.isEquivalence
+        ; isEquivalence₂ = B.Eq₁.isEquivalence
         }
-      ; injective = injective IB.bijective IB.Eq₁.refl IB.Eq₂.sym IB.Eq₂.trans IB.cong
+      ; injective = B.from-injective
       }
-    ; surjective = surjective IB.bijective IB.Eq₁.refl IB.Eq₂.trans
+    ; surjective = B.from-surjective
     }
 
-module _ {≈₁ : Rel A ℓ₁} {f : A → B} (isBij : IsBijection ≈₁ _≡_ f) where
-
-  -- We can always flip a bijection if using the equality over the
-  -- codomain is propositional equality.
-  isBijection-≡ : 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
 
   isCongruent : IsCongruent ≈₁ ≈₂ f → Congruent ≈₂ ≈₁ f⁻¹ → IsCongruent ≈₂ ≈₁ f⁻¹
@@ -111,7 +79,7 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} {f⁻¹ :
   isLeftInverse inv = record
     { isCongruent = isCongruent F.isCongruent F.from-cong
     ; from-cong   = F.to-cong
-    ; inverseˡ    = inverseˡ ≈₁ ≈₂ F.inverseʳ
+    ; inverseˡ    = F.inverseʳ
     } where module F = IsRightInverse inv
 
   isRightInverse : IsLeftInverse ≈₁ ≈₂ f f⁻¹ → IsRightInverse ≈₂ ≈₁ f⁻¹ f
@@ -124,36 +92,18 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} {f⁻¹ :
   isInverse : IsInverse ≈₁ ≈₂ f f⁻¹ → IsInverse ≈₂ ≈₁ f⁻¹ f
   isInverse f-inv = record
     { isLeftInverse = isLeftInverse F.isRightInverse
-    ; inverseʳ      = inverseʳ ≈₁ ≈₂ F.inverseˡ
+    ; inverseʳ      = F.inverseˡ
     } where module F = IsInverse f-inv
 
 ------------------------------------------------------------------------
 -- Setoid bundles
 
-module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} (bij : Bijection R S) where
-
-  private
-    module IB = Bijection bij
-    from      = proj₁ ∘ IB.surjective
-
-  -- We can only flip a bijection if the witness produced by the
-  -- surjection proof respects the equality on the codomain.
-  bijection : Congruent IB.Eq₂._≈_ IB.Eq₁._≈_ from → Bijection S R
-  bijection cong = record
-    { to        = from
-    ; cong      = 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
--- codomain is propositional equality.
-bijection-≡ : {R : Setoid a ℓ₁} {B : Set b} →
-              Bijection R (setoid B) → Bijection (setoid B) R
-bijection-≡ bij = bijection bij (B.Eq₁.reflexive ∘ cong _)
- where module B = Bijection bij
-
 module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} where
 
+  bijection : Bijection R S → Bijection S R
+  bijection bij = record { IsBijection (isBijection B.isBijection) }
+    where module B = Bijection bij
+
   equivalence : Equivalence R S → Equivalence S R
   equivalence equiv = record
     { to        = E.from
@@ -193,7 +143,7 @@ module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} where
 -- Propositional bundles
 
 ⤖-sym : A ⤖ B → B ⤖ A
-⤖-sym b = bijection b (cong _)
+⤖-sym = bijection
 
 ⇔-sym : A ⇔ B → B ⇔ A
 ⇔-sym = equivalence
@@ -214,7 +164,7 @@ module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} where
 -- Please use the new names as continuing support for the old names is
 -- not guaranteed.
 
--- Version v2.0
+-- Version 2.0
 
 sym-⤖ = ⤖-sym
 {-# WARNING_ON_USAGE sym-⤖
diff --git a/src/Function/Properties/Bijection.agda b/src/Function/Properties/Bijection.agda
index c606ad5645..eb9ec0cf7f 100644
--- a/src/Function/Properties/Bijection.agda
+++ b/src/Function/Properties/Bijection.agda
@@ -17,7 +17,6 @@ open import Relation.Binary.Definitions using (Reflexive; Trans)
 open import Relation.Binary.PropositionalEquality.Properties 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
@@ -36,10 +35,8 @@ private
 refl : Reflexive (Bijection {a} {ℓ})
 refl = Identity.bijection _
 
--- Can't prove full symmetry as we have no proof that the witness
--- produced by the surjection proof preserves equality
-sym-≡ : Bijection S (setoid B) → Bijection (setoid B) S
-sym-≡ = Symmetry.bijection-≡
+sym : Bijection S T → Bijection T S
+sym = Symmetry.bijection
 
 trans : Trans (Bijection {a} {ℓ₁} {b} {ℓ₂}) (Bijection {b} {ℓ₂} {c} {ℓ₃}) Bijection
 trans = Composition.bijection
@@ -50,7 +47,7 @@ trans = Composition.bijection
 ⤖-isEquivalence : IsEquivalence {ℓ = ℓ} _⤖_
 ⤖-isEquivalence = record
   { refl  = refl
-  ; sym   = sym-≡
+  ; sym   = sym
   ; trans = trans
   }
 
@@ -59,14 +56,13 @@ trans = Composition.bijection
 
 Bijection⇒Inverse : Bijection S T → Inverse S T
 Bijection⇒Inverse bij = record
-  { to        = to
-  ; from      = to⁻
-  ; to-cong   = cong
-  ; 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]))
+  { to        = B.to
+  ; from      = B.from
+  ; to-cong   = B.cong
+  ; from-cong = B.from-cong
+  ; inverse   = B.inverseˡ , B.inverseʳ
   }
-  where open Bijection bij; to∘to⁻ = proj₂ ∘ strictlySurjective
+  where module B = Bijection bij
 
 Bijection⇒Equivalence : Bijection T S → Equivalence T S
 Bijection⇒Equivalence = Inverse⇒Equivalence ∘ Bijection⇒Inverse
diff --git a/src/Function/Properties/Surjection.agda b/src/Function/Properties/Surjection.agda
index 17b3dc657e..54702c1f13 100644
--- a/src/Function/Properties/Surjection.agda
+++ b/src/Function/Properties/Surjection.agda
@@ -8,17 +8,17 @@
 
 module Function.Properties.Surjection where
 
+open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Function.Base using (_∘_; _$_)
-open import Function.Definitions using (Surjective; Injective; Congruent)
 open import Function.Bundles
-  using (Func; Surjection; _↠_; _⟶_; _↪_; mk↪; _⇔_; mk⇔)
+  using (Func; Surjection; Bijection; _↠_; _⟶_; _↪_; mk↪; _⇔_; mk⇔)
 import Function.Construct.Identity as Identity using (surjection)
 import Function.Construct.Composition as Compose using (surjection)
+open import Function.Definitions using (Surjective; Injective; Congruent)
 open import Level using (Level)
-open import Data.Product.Base using (proj₁; proj₂)
-import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl)
-open import Relation.Binary.Definitions using (Reflexive; Trans)
 open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Definitions using (Reflexive; Trans)
+import Relation.Binary.PropositionalEquality.Core as ≡
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 private
@@ -31,8 +31,8 @@ private
 -- Constructors
 
 mkSurjection : (f : Func S T) (open Func f) →
-              Surjective Eq₁._≈_ Eq₂._≈_ to  →
-              Surjection S T
+               Surjective Eq₁._≈_ Eq₂._≈_ to  →
+               Surjection S T
 mkSurjection f surjective = record
   { Func f
   ; surjective = surjective
@@ -45,11 +45,11 @@ mkSurjection f surjective = record
 ↠⇒⟶ = Surjection.function
 
 ↠⇒↪ : A ↠ B → B ↪ A
-↠⇒↪ s = mk↪ {from = to} λ { ≡.refl → proj₂ (strictlySurjective _)}
+↠⇒↪ s = mk↪ {from = to} λ { ≡.refl → strictlyInverseˡ _ }
   where open Surjection s
 
 ↠⇒⇔ : A ↠ B → A ⇔ B
-↠⇒⇔ s = mk⇔ to (proj₁ ∘ surjective)
+↠⇒⇔ s = mk⇔ to from
   where open Surjection s
 
 ------------------------------------------------------------------------
@@ -63,19 +63,26 @@ trans : Trans (Surjection {a} {ℓ₁} {b} {ℓ₂})
               (Surjection {a} {ℓ₁} {c} {ℓ₃})
 trans = Compose.surjection
 
+
 ------------------------------------------------------------------------
--- Other
-
-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 ≈-Reasoning T
-  open Surjection surj
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.3
+
+module _ (surjection : Surjection S T) where
+
+  open Surjection surjection
 
+  injective⇒to⁻-cong : Injective Eq₁._≈_ Eq₂._≈_ to →
+                       Congruent Eq₂._≈_ Eq₁._≈_ from
+  injective⇒to⁻-cong injective = Bijection.from-cong S⤖T
+    where
+    S⤖T : Bijection S T
+    S⤖T = record { cong = cong ; bijective = injective , surjective }
+{-# WARNING_ON_USAGE injective⇒to⁻-cong
+"Warning: injective⇒to⁻-cong was deprecated in v2.3.
+Please use Function.Bundles.Bijection.from-cong instead. "
+#-}
diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda
index 9533cfb179..6a67f5a4f5 100644
--- a/src/Function/Structures.agda
+++ b/src/Function/Structures.agda
@@ -17,8 +17,10 @@ module Function.Structures {a b ℓ₁ ℓ₂}
   {B : Set b} (_≈₂_ : Rel B ℓ₂) -- Equality over the codomain
   where
 
-open import Data.Product.Base as Product using (∃; _×_; _,_)
+open import Data.Product.Base as Product using (∃; _×_; _,_; proj₁; proj₂)
 open import Function.Base
+open import Function.Consequences.Setoid
+  using (surjective⇒strictlySurjective; inverseˡ⇒surjective; inverseʳ⇒injective)
 open import Function.Definitions
 open import Level using (_⊔_)
 
@@ -59,35 +61,66 @@ record IsInjection (to : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
   open IsCongruent isCongruent public
 
 
-record IsSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+record IsSurjection (to : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
   field
-    isCongruent : IsCongruent f
-    surjective  : Surjective _≈₁_ _≈₂_ f
+    isCongruent : IsCongruent to
+    surjective  : Surjective _≈₁_ _≈₂_ to
 
   open IsCongruent isCongruent public
 
-  strictlySurjective : StrictlySurjective _≈₂_ f
-  strictlySurjective x = Product.map₂ (λ v → v Eq₁.refl) (surjective x)
+  from : B → A
+  from = proj₁ ∘ surjective
+
+  inverseˡ : Inverseˡ _≈₁_ _≈₂_ to from
+  inverseˡ {x = x} = proj₂ (surjective x)
+
+  strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to from
+  strictlyInverseˡ _ = inverseˡ Eq₁.refl
+
+  from-injective : Injective _≈₂_ _≈₁_ from
+  from-injective = Eq₂.trans (Eq₂.sym (strictlyInverseˡ _)) ∘ inverseˡ
 
+  strictlySurjective : StrictlySurjective _≈₂_ to
+  strictlySurjective = surjective⇒strictlySurjective Eq₁.setoid Eq₂.setoid surjective
 
-record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+
+record IsBijection (to : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
   field
-    isInjection : IsInjection f
-    surjective  : Surjective _≈₁_ _≈₂_ f
+    isInjection : IsInjection to
+    surjective  : Surjective _≈₁_ _≈₂_ to
 
   open IsInjection isInjection public
 
-  bijective : Bijective _≈₁_ _≈₂_ f
+  bijective : Bijective _≈₁_ _≈₂_ to
   bijective = injective , surjective
 
-  isSurjection : IsSurjection f
+  isSurjection : IsSurjection to
   isSurjection = record
     { isCongruent = isCongruent
     ; surjective  = surjective
     }
 
   open IsSurjection isSurjection public
-    using (strictlySurjective)
+    using (from; from-injective; strictlySurjective; inverseˡ; strictlyInverseˡ)
+
+  private
+    y≈z⇒to∘from[y]≡z : ∀ {y z} → y ≈₂ z → to (from y) ≈₂ z
+    y≈z⇒to∘from[y]≡z = Eq₂.trans (strictlyInverseˡ _)
+
+  inverseʳ : Inverseʳ _≈₁_ _≈₂_ to from
+  inverseʳ = injective ∘ y≈z⇒to∘from[y]≡z
+
+  strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to from
+  strictlyInverseʳ = injective ∘ strictlyInverseˡ ∘ to
+
+  from-cong : Congruent _≈₂_ _≈₁_ from
+  from-cong = inverseʳ ∘ Eq₂.sym ∘ y≈z⇒to∘from[y]≡z ∘ Eq₂.sym
+
+  from-surjective : Surjective _≈₂_ _≈₁_ from
+  from-surjective = inverseˡ⇒surjective Eq₂.setoid Eq₁.setoid inverseʳ
+
+  from-bijective : Bijective _≈₂_ _≈₁_ from
+  from-bijective = from-injective , from-surjective
 
 
 ------------------------------------------------------------------------
@@ -104,12 +137,14 @@ record IsLeftInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ 
     renaming (cong to to-cong)
 
   strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to from
-  strictlyInverseˡ x = inverseˡ Eq₁.refl
+  strictlyInverseˡ _ = inverseˡ Eq₁.refl
+
+  surjective = inverseˡ⇒surjective Eq₁.setoid Eq₂.setoid inverseˡ
 
   isSurjection : IsSurjection to
   isSurjection = record
     { isCongruent = isCongruent
-    ; surjective = λ y → from y , inverseˡ
+    ; surjective = surjective
     }
 
 
@@ -123,7 +158,16 @@ record IsRightInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁
     renaming (cong to to-cong)
 
   strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to from
-  strictlyInverseʳ x = inverseʳ Eq₂.refl
+  strictlyInverseʳ _ = inverseʳ Eq₂.refl
+
+  injective : Injective _≈₁_ _≈₂_ to
+  injective = inverseʳ⇒injective Eq₁.setoid Eq₂.setoid to inverseʳ
+
+  isInjection : IsInjection to
+  isInjection = record
+    { isCongruent = isCongruent
+    ; injective   = injective
+    }
 
 
 record IsInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
@@ -181,9 +225,9 @@ record IsBiInverse
 
 -- See the comment on `SplitSurjection` in `Function.Bundles` for an
 -- explanation of (split) surjections.
-record IsSplitSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+record IsSplitSurjection (to : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
   field
     from : B → A
-    isLeftInverse : IsLeftInverse f from
+    isLeftInverse : IsLeftInverse to from
 
   open IsLeftInverse isLeftInverse public