diff --git a/CHANGELOG.md b/CHANGELOG.md
index f13d2635cb..11dec8b9f4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,6 +6,11 @@ The library has been tested using Agda 2.7.0 and 2.7.0.1.
 Highlights
 ----------
 
+* A major overhaul of the `Function` hierarchy sees the systematic development
+  and use of theory of the left inverse `from` to a given `Surjective` function
+  `to`, in `Function.Consequences.Section`, up to and including full symmetry of
+  `Bijection`, in `Function.Properties.Bijection`.
+
 Bug-fixes
 ---------
 
@@ -88,6 +93,32 @@ 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.Construct.Symmetry`:
+  ```agda
+  injective       ↦  Function.Consequences.Section.injective
+  surjective      ↦  Function.Consequences.Section.surjective
+  bijective       ↦  Function.Consequences.Section.bijective
+  isBijection     ↦  isBijectionWithoutCongruence
+  isBijection-≡   ↦  isBijectionWithoutCongruence
+  bijection-≡     ↦  bijectionWithoutCongruence
+  ```
+
+* In `Function.Properties.Bijection`:
+  ```agda
+  sym-≡   ↦  sym
+  ```
+
+* In `Function.Properties.Surjection`:
+  ```agda
+  injective⇒to⁻-cong   ↦  Function.Construct.Symmetry.bijectionWithoutCongruence
+  ```
+
 New modules
 -----------
 
@@ -126,3 +157,77 @@ Additions to existing modules
   quasiring                       : Quasiring c ℓ → Quasiring (a ⊔ c) (a ⊔ ℓ)
   commutativeRing                 : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ)
   ```
+
+* 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.Consequences` and `Function.Consequences.Setoid`:
+  the theory of the left inverse of a surjective function `to`
+  ```agda
+  module Section (surj :  Surjective ≈₁ ≈₂ to)
+  ```
+
+* In `Function.Construct.Symmetry`:
+  ```agda
+  isBijectionWithoutCongruence : IsBijection ≈₁ ≈₂ to → IsBijection ≈₂ ≈₁ from
+  bijectionWithoutCongruence   : 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
+  ```
+
+* 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
+  ```
+
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 6532715a21..da22fdd763 100644
--- a/src/Function/Bundles.agda
+++ b/src/Function/Bundles.agda
@@ -20,16 +20,16 @@
 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
@@ -113,13 +113,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
@@ -146,8 +157,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
@@ -155,7 +173,8 @@ 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ʳ)
 
 
 ------------------------------------------------------------------------
@@ -220,6 +239,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
@@ -236,7 +257,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
     surjection = record
       { to = to
       ; cong = to-cong
-      ; surjective = λ y → from y , inverseˡ
+      ; surjective = surjective
       }
 
 
@@ -246,7 +267,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
@@ -264,7 +285,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
@@ -272,6 +295,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
@@ -370,7 +400,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..d31766e55a 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,16 @@ private
     a b ℓ₁ ℓ₂ : Level
     A B : Set a
     ≈₁ ≈₂ : Rel A ℓ₁
-    f f⁻¹ : A → B
+    to 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 +41,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 +52,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ᵇ
@@ -68,16 +70,15 @@ inverseᵇ⇒bijective {f = f} ≈₂ refl sym trans (invˡ , invʳ) =
 -- StrictlySurjective
 
 surjective⇒strictlySurjective : ∀ (≈₂ : Rel B ℓ₂) →
-                                 Reflexive ≈₁ →
-                                 Surjective ≈₁ ≈₂ f →
-                                 StrictlySurjective ≈₂ f
-surjective⇒strictlySurjective _ refl surj x =
-  Product.map₂ (λ v → v refl) (surj x)
+                                Reflexive ≈₁ →
+                                Surjective ≈₁ ≈₂ f →
+                                StrictlySurjective ≈₂ f
+surjective⇒strictlySurjective _ refl surj = Product.map₂ (λ v → v refl) ∘ surj
 
 strictlySurjective⇒surjective : Transitive ≈₂ →
-                                 Congruent ≈₁ ≈₂ f →
-                                 StrictlySurjective ≈₂ f →
-                                 Surjective ≈₁ ≈₂ f
+                                Congruent ≈₁ ≈₂ f →
+                                StrictlySurjective ≈₂ f →
+                                Surjective ≈₁ ≈₂ f
 strictlySurjective⇒surjective trans cong surj x =
   Product.map₂ (λ fy≈x z≈y → trans (cong z≈y) fy≈x) (surj x)
 
@@ -104,11 +105,53 @@ 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}
+
+------------------------------------------------------------------------
+-- Theory of the section of a Surjective function
+
+module Section (≈₂ : Rel B ℓ₂) (surj :  Surjective {A = A} ≈₁ ≈₂ to) where
+
+  from : B → A
+  from = proj₁ ∘ surj
+
+  inverseˡ : Inverseˡ ≈₁ ≈₂ to from
+  inverseˡ {x = x} = proj₂ (surj x)
+
+  module _ (refl : Reflexive ≈₁) where
+
+    strictlySurjective : StrictlySurjective ≈₂ to
+    strictlySurjective = surjective⇒strictlySurjective ≈₂ refl surj
+
+    strictlyInverseˡ : StrictlyInverseˡ ≈₂ to from
+    strictlyInverseˡ _ = inverseˡ refl
+
+    injective : Symmetric ≈₂ → Transitive ≈₂ → Injective ≈₂ ≈₁ from
+    injective sym trans = trans (sym (strictlyInverseˡ _)) ∘ inverseˡ
+
+  module _ (inj : Injective ≈₁ ≈₂ to) (refl : Reflexive ≈₁) where
+
+    private to∘from≡id = strictlyInverseˡ refl
+
+    cong : Symmetric ≈₂ → Transitive ≈₂ → Congruent ≈₂ ≈₁ from
+    cong sym trans = inj ∘ trans (to∘from≡id _) ∘ sym ∘ trans (to∘from≡id _) ∘ sym
+
+    inverseʳ : Transitive ≈₂ → Inverseʳ ≈₁ ≈₂ to from
+    inverseʳ trans = inj ∘ trans (to∘from≡id _)
+
+    strictlyInverseʳ : Reflexive ≈₂ → Transitive ≈₂ → StrictlyInverseʳ ≈₁ to from
+    strictlyInverseʳ refl trans _ = inverseʳ trans refl
+
+    surjective : Transitive ≈₂ → Surjective ≈₂ ≈₁ from
+    surjective trans x = to x , inverseʳ trans
+
+    bijective : Symmetric ≈₂ → Transitive ≈₂ → Bijective ≈₂ ≈₁ from
+    bijective sym trans = injective refl sym trans , surjective trans
diff --git a/src/Function/Consequences/Propositional.agda b/src/Function/Consequences/Propositional.agda
index a2558a9c48..17d665e898 100644
--- a/src/Function/Consequences/Propositional.agda
+++ b/src/Function/Consequences/Propositional.agda
@@ -11,14 +11,20 @@ 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
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Relation.Binary.PropositionalEquality.Properties
   using (setoid)
-open import Function.Definitions
-open import Relation.Nullary.Negation.Core using (contraposition)
 
 import Function.Consequences.Setoid (setoid A) (setoid B) as Setoid
 
+private
+  variable
+    f : A → B
+    f⁻¹ : B → A
+
+
 ------------------------------------------------------------------------
 -- Re-export setoid properties
 
@@ -32,22 +38,15 @@ open Setoid public
 ------------------------------------------------------------------------
 -- Properties that rely on congruence
 
-private
-  variable
-    f : A → B
-    f⁻¹ : B → A
-
 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/Consequences/Setoid.agda b/src/Function/Consequences/Setoid.agda
index d2c3b948d9..e2237f4fff 100644
--- a/src/Function/Consequences/Setoid.agda
+++ b/src/Function/Consequences/Setoid.agda
@@ -25,9 +25,10 @@ private
   open module T = Setoid T using () renaming (Carrier to B; _≈_ to ≈₂)
 
   variable
-    f : A → B
+    to f : A → B
     f⁻¹ : B → A
 
+
 ------------------------------------------------------------------------
 -- Injective
 
@@ -90,3 +91,38 @@ strictlyInverseʳ⇒inverseʳ : Congruent ≈₂ ≈₁ f⁻¹ →
                             StrictlyInverseʳ ≈₁ f f⁻¹ →
                             Inverseʳ ≈₁ ≈₂ f f⁻¹
 strictlyInverseʳ⇒inverseʳ = C.strictlyInverseʳ⇒inverseʳ S.trans
+
+------------------------------------------------------------------------
+-- Section
+
+module Section (surj :  Surjective ≈₁ ≈₂ to) where
+
+  private module From = C.Section ≈₂ surj
+
+  open From public using (from; inverseˡ)
+
+  strictlySurjective : StrictlySurjective ≈₂ to
+  strictlySurjective = From.strictlySurjective S.refl
+
+  strictlyInverseˡ : StrictlyInverseˡ ≈₂ to from
+  strictlyInverseˡ = From.strictlyInverseˡ S.refl
+
+  injective : Injective ≈₂ ≈₁ from
+  injective = From.injective S.refl T.sym T.trans
+
+  module _ (inj : Injective ≈₁ ≈₂ to) where
+
+    cong : Congruent ≈₂ ≈₁ from
+    cong = From.cong inj S.refl T.sym T.trans
+
+    inverseʳ : Inverseʳ ≈₁ ≈₂ to from
+    inverseʳ = From.inverseʳ inj S.refl T.trans
+
+    strictlyInverseʳ : StrictlyInverseʳ ≈₁ to from
+    strictlyInverseʳ = From.strictlyInverseʳ inj S.refl T.refl T.trans
+
+    surjective : Surjective ≈₂ ≈₁ from
+    surjective = From.surjective inj S.refl T.trans
+
+    bijective : Bijective ≈₂ ≈₁ from
+    bijective = From.bijective inj S.refl T.sym T.trans
diff --git a/src/Function/Construct/Composition.agda b/src/Function/Construct/Composition.agda
index 10289cc8c9..799c0257c7 100644
--- a/src/Function/Construct/Composition.agda
+++ b/src/Function/Construct/Composition.agda
@@ -40,9 +40,10 @@ module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) (≈₃ : Rel C ℓ₃)
 
   surjective : Surjective ≈₁ ≈₂ f → Surjective ≈₂ ≈₃ g →
                Surjective ≈₁ ≈₃ (g ∘ f)
-  surjective f-sur g-sur x with g-sur x
-  ... | y , gproof with f-sur y
-  ...   | z , fproof = z , gproof ∘ fproof
+  surjective f-sur g-sur x =
+    let y , gproof = g-sur x in
+    let z , fproof = f-sur y in
+        z , gproof ∘ fproof
 
   bijective : Bijective ≈₁ ≈₂ f → Bijective ≈₂ ≈₃ g →
               Bijective ≈₁ ≈₃ (g ∘ f)
diff --git a/src/Function/Construct/Symmetry.agda b/src/Function/Construct/Symmetry.agda
index e7e9f13db9..810b058aa4 100644
--- a/src/Function/Construct/Symmetry.agda
+++ b/src/Function/Construct/Symmetry.agda
@@ -8,8 +8,10 @@
 
 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.Consequences
+  using (module Section)
 open import Function.Definitions
   using (Bijective; Injective; Surjective; Inverseˡ; Inverseʳ; Inverseᵇ; Congruent)
 open import Function.Structures
@@ -20,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
@@ -31,70 +33,40 @@ 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
+  -- We can ALWAYS flip a bijection, WITHOUT knowing the witness produced
+  -- by the surjection proof respects the equality on the codomain.
+  isBijectionWithoutCongruence : IsBijection ≈₂ ≈₁ B.from
+  isBijectionWithoutCongruence = record
     { isInjection = record
       { isCongruent = record
-        { cong           = f⁻¹-cong
-        ; isEquivalence₁ = IB.Eq₂.isEquivalence
-        ; isEquivalence₂ = IB.Eq₁.isEquivalence
+        { cong           = S.cong B.injective B.Eq₁.refl B.Eq₂.sym B.Eq₂.trans
+        ; isEquivalence₁ = B.Eq₂.isEquivalence
+        ; isEquivalence₂ = B.Eq₁.isEquivalence
         }
-      ; injective = injective IB.bijective IB.Eq₁.refl IB.Eq₂.sym IB.Eq₂.trans IB.cong
+      ; injective = S.injective B.Eq₁.refl B.Eq₂.sym B.Eq₂.trans
       }
-    ; surjective = surjective IB.bijective IB.Eq₁.refl IB.Eq₂.trans
-    }
-
-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
+    ; surjective = S.surjective B.injective B.Eq₁.refl B.Eq₂.trans
+    } where module S = Section ≈₂ B.surjective
 
 module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} {f⁻¹ : B → A} where
 
@@ -109,7 +81,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
@@ -122,7 +94,7 @@ 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
 
 ------------------------------------------------------------------------
@@ -130,25 +102,12 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} {f⁻¹ :
 
 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
+  -- We can always flip a bijection WITHOUT knowing if the witness produced
+  -- by the surjection proof respects the equality on the codomain.
+  bijectionWithoutCongruence : Bijection S R
+  bijectionWithoutCongruence = record {
+      IsBijection (isBijectionWithoutCongruence B.isBijection)
+    } where module B = Bijection bij
 
 module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} where
 
@@ -191,7 +150,7 @@ module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} where
 -- Propositional bundles
 
 ⤖-sym : A ⤖ B → B ⤖ A
-⤖-sym b = bijection b (cong _)
+⤖-sym = bijectionWithoutCongruence
 
 ⇔-sym : A ⇔ B → B ⇔ A
 ⇔-sym = equivalence
@@ -212,7 +171,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-⤖
@@ -243,3 +202,68 @@ sym-↔ = ↔-sym
 "Warning: sym-↔ was deprecated in v2.0.
 Please use ↔-sym instead."
 #-}
+
+-- Version 2.3
+
+module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B}
+         ((inj , surj) : Bijective ≈₁ ≈₂ f) (refl : Reflexive ≈₁)
+         where
+
+  private
+    module S = Section ≈₂ surj
+
+  injective : Symmetric ≈₂ → Transitive ≈₂ →
+              Congruent ≈₁ ≈₂ f → Injective ≈₂ ≈₁ S.from
+  injective sym trans _ = S.injective refl sym trans
+
+  surjective : Transitive ≈₂ → Surjective ≈₂ ≈₁ S.from
+  surjective = S.surjective inj refl
+
+  bijective : Symmetric ≈₂ → Transitive ≈₂ →
+              Congruent ≈₁ ≈₂ f → Bijective ≈₂ ≈₁ S.from
+  bijective sym trans cong = injective sym trans cong , surjective trans
+{-# WARNING_ON_USAGE injective
+"Warning: injective was deprecated in v2.3.
+Please use Function.Consequences.Section.injective instead, with a sharper type."
+#-}
+{-# WARNING_ON_USAGE surjective
+"Warning: surjective was deprecated in v2.3.
+Please use Function.Consequences.Section.surjective instead."
+#-}
+{-# WARNING_ON_USAGE bijective
+"Warning: bijective was deprecated in v2.3.
+Please use Function.Consequences.Section.bijective instead, with a sharper type."
+#-}
+
+module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B}
+         (isBij : IsBijection ≈₁ ≈₂ f)
+         where
+  private module B = IsBijection isBij
+  isBijection : Congruent ≈₂ ≈₁ B.from → IsBijection ≈₂ ≈₁ B.from
+  isBijection _ = isBijectionWithoutCongruence isBij
+{-# WARNING_ON_USAGE isBijection
+"Warning: isBijection was deprecated in v2.3.
+Please use isBijectionWithoutCongruence instead, with a sharper type."
+#-}
+
+module _ {≈₁ : Rel A ℓ₁} {f : A → B} (isBij : IsBijection ≈₁ _≡_ f) where
+  isBijection-≡ : IsBijection _≡_ ≈₁ _
+  isBijection-≡ = isBijectionWithoutCongruence isBij
+{-# WARNING_ON_USAGE isBijection-≡
+"Warning: isBijection-≡ was deprecated in v2.3.
+Please use isBijectionWithoutCongruence instead, with a sharper type."
+#-}
+
+module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} (bij : Bijection R S) where
+  private module B = Bijection bij
+  bijection : Congruent B.Eq₂._≈_ B.Eq₁._≈_ B.from → Bijection S R
+  bijection _ = bijectionWithoutCongruence bij
+
+bijection-≡ : {R : Setoid a ℓ₁} {B : Set b} →
+              Bijection R (setoid B) → Bijection (setoid B) R
+bijection-≡ = bijectionWithoutCongruence
+{-# WARNING_ON_USAGE bijection-≡
+"Warning: bijection-≡ was deprecated in v2.3.
+Please use bijectionWithoutCongruence instead, with a sharper type."
+#-}
+
diff --git a/src/Function/Properties/Bijection.agda b/src/Function/Properties/Bijection.agda
index 21e295e807..ca560f77bd 100644
--- a/src/Function/Properties/Bijection.agda
+++ b/src/Function/Properties/Bijection.agda
@@ -17,8 +17,8 @@ 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)
+open import Function.Properties.Inverse
+  using (Inverse⇒Bijection; Inverse⇒Equivalence)
 
 import Function.Construct.Identity as Identity
 import Function.Construct.Symmetry as Symmetry
@@ -36,43 +36,60 @@ 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-≡
+-- Now we *can* prove full symmetry as we now have a proof that
+-- the witness produced by the surjection proof preserves equality
+sym : Bijection S T → Bijection T S
+sym = Symmetry.bijectionWithoutCongruence
 
 trans : Trans (Bijection {a} {ℓ₁} {b} {ℓ₂}) (Bijection {b} {ℓ₂} {c} {ℓ₃}) Bijection
 trans = Composition.bijection
 
-------------------------------------------------------------------------
--- Propositional properties
-
-⤖-isEquivalence : IsEquivalence {ℓ = ℓ} _⤖_
-⤖-isEquivalence = record
-  { refl  = refl
-  ; sym   = sym-≡
-  ; trans = trans
-  }
-
 ------------------------------------------------------------------------
 -- Conversion functions
 
 Bijection⇒Inverse : Bijection S T → Inverse S T
 Bijection⇒Inverse bij = record
   { to        = to
-  ; from      = to⁻
+  ; from      = Bijection.to (sym bij)
   ; 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]))
+  ; from-cong = Bijection.cong (sym bij)
+  ; inverse   = inverseˡ , inverseʳ
+
   }
-  where open Bijection bij; to∘to⁻ = proj₂ ∘ strictlySurjective
+  where open Bijection bij
 
 Bijection⇒Equivalence : Bijection T S → Equivalence T S
 Bijection⇒Equivalence = Inverse⇒Equivalence ∘ Bijection⇒Inverse
 
+------------------------------------------------------------------------
+-- Propositional properties
+
+⤖-isEquivalence : IsEquivalence {ℓ = ℓ} _⤖_
+⤖-isEquivalence = record
+  { refl  = refl
+  ; sym   = sym
+  ; trans = trans
+  }
+
 ⤖⇒↔ : A ⤖ B → A ↔ B
 ⤖⇒↔ = Bijection⇒Inverse
 
 ⤖⇒⇔ : A ⤖ B → A ⇔ B
 ⤖⇒⇔ = Bijection⇒Equivalence
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.3
+
+open Symmetry public
+  using ()
+  renaming (bijection-≡ to sym-≡)
+{-# WARNING_ON_USAGE sym-≡
+"Warning: sym-≡ was deprecated in v2.3.
+Please use sym instead. "
+#-}
diff --git a/src/Function/Properties/Surjection.agda b/src/Function/Properties/Surjection.agda
index d5e6b8e75d..1a22e0a81f 100644
--- a/src/Function/Properties/Surjection.agda
+++ b/src/Function/Properties/Surjection.agda
@@ -10,12 +10,13 @@ module Function.Properties.Surjection where
 
 open import Function.Base using (_∘_; _$_)
 open import Function.Definitions using (Surjective; Injective; Congruent)
-open import Function.Bundles using (Func; Surjection; _↠_; _⟶_; _↪_; mk↪;
-  _⇔_; mk⇔)
+open import Function.Bundles
+  using (Func; Surjection; Bijection; _↠_; _⟶_; _↪_; mk↪; _⇔_; mk⇔)
 import Function.Construct.Identity as Identity
+import Function.Construct.Symmetry as Symmetry
 import Function.Construct.Composition as Compose
 open import Level using (Level)
-open import Data.Product.Base using (proj₁; proj₂)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
 import Relation.Binary.PropositionalEquality.Core as ≡
 open import Relation.Binary.Definitions using (Reflexive; Trans)
 open import Relation.Binary.Bundles using (Setoid)
@@ -31,8 +32,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 +46,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 +64,28 @@ 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 = from-cong
+    where
+    SB : Bijection S T
+    SB = record { cong = cong ; bijective = injective , surjective }
+    open Bijection (Symmetry.bijectionWithoutCongruence SB)
+      using () renaming (cong to from-cong)
+{-# WARNING_ON_USAGE injective⇒to⁻-cong
+"Warning: injective⇒to⁻-cong was deprecated in v2.3.
+Please use Function.Construct.Symmetry.bijectionWithoutCongruence instead. "
+#-}
diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda
index 9533cfb179..0cb62011d3 100644
--- a/src/Function/Structures.agda
+++ b/src/Function/Structures.agda
@@ -19,6 +19,7 @@ module Function.Structures {a b ℓ₁ ℓ₂}
 
 open import Data.Product.Base as Product using (∃; _×_; _,_)
 open import Function.Base
+open import Function.Consequences.Setoid
 open import Function.Definitions
 open import Level using (_⊔_)
 
@@ -59,35 +60,43 @@ 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)
+  open Section Eq₁.setoid Eq₂.setoid surjective public
+    using (from; inverseˡ; strictlyInverseˡ; strictlySurjective)
 
 
-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)
+  private module S = Section Eq₁.setoid Eq₂.setoid surjective
+
+  open S public
+    using (strictlySurjective; from; inverseˡ; strictlyInverseˡ)
+
+  inverseʳ : Inverseʳ _≈₁_ _≈₂_ to from
+  inverseʳ = S.inverseʳ injective
+
+  strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to from
+  strictlyInverseʳ = S.strictlyInverseʳ injective
 
 
 ------------------------------------------------------------------------
@@ -104,12 +113,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 +134,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 +201,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