From 598240208c4e737469bc241da6fcf7bd072882d6 Mon Sep 17 00:00:00 2001
From: Chris Pollard <cspollard@gmail.com>
Date: Thu, 17 Apr 2025 13:35:54 +0100
Subject: [PATCH 1/7] add RightInverse to
 Data.Product.Function.Dependent.Propositional

---
 src/Data/Product/Function/Dependent/Propositional.agda | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/Data/Product/Function/Dependent/Propositional.agda b/src/Data/Product/Function/Dependent/Propositional.agda
index 4c6f391e2f..70eaa97cf2 100644
--- a/src/Data/Product/Function/Dependent/Propositional.agda
+++ b/src/Data/Product/Function/Dependent/Propositional.agda
@@ -28,6 +28,7 @@ open import Function.Bundles
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 open import Relation.Binary.PropositionalEquality.Properties as ≡
   using (module ≡-Reasoning)
+open import Function.Construct.Symmetry using (↩-sym; ↪-sym)
 
 private
   variable
@@ -238,6 +239,14 @@ module _ where
 ------------------------------------------------------------------------
 -- Right inverses
 
+module _ where
+  open RightInverse
+
+  -- the dual to Σ-↩, taking advantage of the proof above by threading
+  -- relevant symmetry proofs through it.
+  Σ-↪ : (I↪J : I ↪ J) → (∀ {j} → A (from I↪J j) ↪ B j) → Σ I A ↪ Σ J B
+  Σ-↪ I↪J A↪B = ↩-sym (Σ-↩ (↪-sym I↪J) (↪-sym A↪B))
+
 ------------------------------------------------------------------------
 -- Inverses
 

From 627b36854db0f8ec813c063880b7bf45f2ce2f79 Mon Sep 17 00:00:00 2001
From: Chris Pollard <cspollard@gmail.com>
Date: Thu, 17 Apr 2025 13:37:25 +0100
Subject: [PATCH 2/7] correct naming of left-inverse

---
 src/Data/Product/Function/Dependent/Setoid.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/Product/Function/Dependent/Setoid.agda b/src/Data/Product/Function/Dependent/Setoid.agda
index 0ad3785ed7..a82a345568 100644
--- a/src/Data/Product/Function/Dependent/Setoid.agda
+++ b/src/Data/Product/Function/Dependent/Setoid.agda
@@ -185,11 +185,11 @@ module _ where
   open RightInverse
   open Setoid
 
-  left-inverse :
+  right-inverse :
     (I↪J : I ↪ J) →
     (∀ {j} → RightInverse (A atₛ (from I↪J j)) (B atₛ j)) →
     RightInverse (I ×ₛ A) (J ×ₛ B)
-  left-inverse {I = I} {J = J} {A = A} {B = B} I↪J A↪B =
+  right-inverse {I = I} {J = J} {A = A} {B = B} I↪J A↪B =
     mkRightInverse equiv invʳ
     where
     equiv : Equivalence (I ×ₛ A) (J ×ₛ B)

From 5c2a906bb201a881ef638c0538f52adf29cab86a Mon Sep 17 00:00:00 2001
From: Chris Pollard <cspollard@gmail.com>
Date: Fri, 18 Apr 2025 10:05:14 +0100
Subject: [PATCH 3/7] add leftInverse

---
 .../Product/Function/Dependent/Setoid.agda    | 36 ++++++++++++++++---
 1 file changed, 32 insertions(+), 4 deletions(-)

diff --git a/src/Data/Product/Function/Dependent/Setoid.agda b/src/Data/Product/Function/Dependent/Setoid.agda
index a82a345568..fc6e5c0b84 100644
--- a/src/Data/Product/Function/Dependent/Setoid.agda
+++ b/src/Data/Product/Function/Dependent/Setoid.agda
@@ -1,4 +1,4 @@
-------------------------------------------------------------------------
+-----------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Dependent product combinators for setoid equality preserving
@@ -20,6 +20,7 @@ open import Function.Properties.Injection using (mkInjection)
 open import Function.Properties.Surjection using (mkSurjection; ↠⇒⇔)
 open import Function.Properties.Equivalence using (mkEquivalence; ⇔⇒⟶; ⇔⇒⟵)
 open import Function.Properties.RightInverse using (mkRightInverse)
+import Function.Construct.Symmetry as Sym
 open import Relation.Binary.Core using (_=[_]⇒_)
 open import Relation.Binary.Bundles as B
 open import Relation.Binary.Indexed.Heterogeneous
@@ -179,17 +180,17 @@ module _ where
     surj = strictlySurjective⇒surjective (I ×ₛ A) (J ×ₛ B) (Func.cong func) strictlySurj
 
 ------------------------------------------------------------------------
--- LeftInverse
+-- RightInverse
 
 module _ where
   open RightInverse
   open Setoid
 
-  right-inverse :
+  rightInverse :
     (I↪J : I ↪ J) →
     (∀ {j} → RightInverse (A atₛ (from I↪J j)) (B atₛ j)) →
     RightInverse (I ×ₛ A) (J ×ₛ B)
-  right-inverse {I = I} {J = J} {A = A} {B = B} I↪J A↪B =
+  rightInverse {I = I} {J = J} {A = A} {B = B} I↪J A↪B =
     mkRightInverse equiv invʳ
     where
     equiv : Equivalence (I ×ₛ A) (J ×ₛ B)
@@ -201,6 +202,19 @@ module _ where
     invʳ : Inverseʳ (_≈_ (I ×ₛ A)) (_≈_ (J ×ₛ B)) (Equivalence.to equiv) (Equivalence.from equiv)
     invʳ = strictlyInverseʳ⇒inverseʳ (I ×ₛ A) (J ×ₛ B) (Equivalence.from-cong equiv) strictlyInvʳ
 
+------------------------------------------------------------------------
+-- LeftInverse
+
+module _ where
+  open LeftInverse
+  open Setoid
+
+  leftInverse :
+    (I↩J : I ↩ J) →
+    (∀ {i} → LeftInverse (A atₛ i) (B atₛ (to I↩J i))) →
+    LeftInverse (I ×ₛ A) (J ×ₛ B)
+  leftInverse {I = I} {J = J} {A = A} {B = B} I↩J A↩B =
+    Sym.leftInverse (rightInverse (Sym.rightInverse I↩J) (Sym.rightInverse A↩B))
 
 ------------------------------------------------------------------------
 -- Inverses
@@ -252,3 +266,17 @@ module _ where
     invʳ : Inverseʳ (_≈_ (I ×ₛ A)) (_≈_ (J ×ₛ B)) to′ from′
     invʳ = strictlyInverseʳ⇒inverseʳ (I ×ₛ A) (J ×ₛ B) from′-cong strictlyInvʳ
 
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.3
+
+left-inverse = rightInverse
+{-# WARNING_ON_USAGE left-inverse
+"Warning: left-inverse was deprecated in v2.3.
+Please use rightInverse or leftInverse instead."
+#-}
\ No newline at end of file

From 8bec46b9ab912d9fe7620f575421e5d708804bce Mon Sep 17 00:00:00 2001
From: Chris Pollard <cspollard@gmail.com>
Date: Fri, 18 Apr 2025 10:07:54 +0100
Subject: [PATCH 4/7] update changelog

---
 CHANGELOG.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index c59957a7fe..2e83d581ee 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -17,6 +17,11 @@ 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`.
 
+* In `Data.Product.Function.Dependent.Setoid`, `left-inverse` defined a
+  `RightInverse`.
+  This has been deprecated in favor or `rightInverse`, and a corrected (and
+  correctly-named) function `leftInverse` has been added.
+
 Non-backwards compatible changes
 --------------------------------
 

From ca2c9d144eb205c99760d60409939cb371107806 Mon Sep 17 00:00:00 2001
From: Chris Pollard <cspollard@gmail.com>
Date: Fri, 18 Apr 2025 10:46:38 +0100
Subject: [PATCH 5/7] whitespace

---
 src/Data/Product/Function/Dependent/Setoid.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Product/Function/Dependent/Setoid.agda b/src/Data/Product/Function/Dependent/Setoid.agda
index fc6e5c0b84..cb7fa89c22 100644
--- a/src/Data/Product/Function/Dependent/Setoid.agda
+++ b/src/Data/Product/Function/Dependent/Setoid.agda
@@ -279,4 +279,4 @@ left-inverse = rightInverse
 {-# WARNING_ON_USAGE left-inverse
 "Warning: left-inverse was deprecated in v2.3.
 Please use rightInverse or leftInverse instead."
-#-}
\ No newline at end of file
+#-}

From 4052b6144c79f4113156995ec6671547060bed07 Mon Sep 17 00:00:00 2001
From: Chris Pollard <cspollard@gmail.com>
Date: Fri, 18 Apr 2025 10:53:29 +0100
Subject: [PATCH 6/7] forgot to finish CHANGELOG

---
 CHANGELOG.md | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2e83d581ee..bc08881066 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -36,6 +36,8 @@ Minor improvements
 * Moved the concept `Irrelevant` of irrelevance (h-proposition) from `Relation.Nullary`
   to its own dedicated module `Relation.Nullary.Irrelevant`.
 
+* Added `Σ-↪` in `Data.Product.Function.Dependent.Propositional`.
+
 Deprecated modules
 ------------------
 
@@ -139,6 +141,11 @@ Deprecated names
   product-↭   ↦  Data.Nat.ListAction.Properties.product-↭
   ```
 
+* In `Data.Product.Function.Dependent.Setoid`:
+  ```agda
+  left-inverse ↦ rightInverse
+  ```
+
 New modules
 -----------
 

From 4fcc8b2fcad9de5243ca3097ff4fa10710f5aa12 Mon Sep 17 00:00:00 2001
From: Chris Pollard <cspollard@gmail.com>
Date: Fri, 18 Apr 2025 12:14:13 +0100
Subject: [PATCH 7/7] james suggestions

---
 CHANGELOG.md                                  | 20 +++++++++++++++++--
 .../Product/Function/Dependent/Setoid.agda    |  2 +-
 2 files changed, 19 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index bc08881066..ba601e31d3 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -36,8 +36,6 @@ Minor improvements
 * Moved the concept `Irrelevant` of irrelevance (h-proposition) from `Relation.Nullary`
   to its own dedicated module `Relation.Nullary.Irrelevant`.
 
-* Added `Σ-↪` in `Data.Product.Function.Dependent.Propositional`.
-
 Deprecated modules
 ------------------
 
@@ -244,6 +242,24 @@ Additions to existing modules
   filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys
   ```
 
+* In `Data.Product.Function.Dependent.Propositional`:
+  ```agda
+  Σ-↪ : (I↪J : I ↪ J) → (∀ {j} → A (from I↪J j) ↪ B j) → Σ I A ↪ Σ J B
+  ```
+
+* In `Data.Product.Function.Dependent.Setoid`:
+  ```agda
+  rightInverse :
+     (I↪J : I ↪ J) →
+     (∀ {j} → RightInverse (A atₛ (from I↪J j)) (B atₛ j)) →
+     RightInverse (I ×ₛ A) (J ×ₛ B)
+
+  leftInverse :
+    (I↩J : I ↩ J) →
+    (∀ {i} → LeftInverse (A atₛ i) (B atₛ (to I↩J i))) →
+    LeftInverse (I ×ₛ A) (J ×ₛ B)
+  ```
+
 * In `Data.Vec.Relation.Binary.Pointwise.Inductive`:
   ```agda
   zipWith-assoc : Associative _∼_ f → Associative (Pointwise _∼_) (zipWith {n = n} f)
diff --git a/src/Data/Product/Function/Dependent/Setoid.agda b/src/Data/Product/Function/Dependent/Setoid.agda
index cb7fa89c22..205f928d8f 100644
--- a/src/Data/Product/Function/Dependent/Setoid.agda
+++ b/src/Data/Product/Function/Dependent/Setoid.agda
@@ -1,4 +1,4 @@
------------------------------------------------------------------------
+------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Dependent product combinators for setoid equality preserving