Add/fix RightInverse for dependent products (#2706)

* add RightInverse to Data.Product.Function.Dependent.Propositional

* correct naming of left-inverse

* add leftInverse

* update changelog

* whitespace

* forgot to finish CHANGELOG

* james suggestions

Author: cspollard

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
 --------------------------------
 
@@ -134,6 +139,11 @@ Deprecated names
   product-↭   ↦  Data.Nat.ListAction.Properties.product-↭
   ```
 
+* In `Data.Product.Function.Dependent.Setoid`:
+  ```agda
+  left-inverse ↦ rightInverse
+  ```
+
 New modules
 -----------
 
@@ -232,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)

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
 

src/Data/Product/Function/Dependent/Setoid.agda

@@ -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
 
-  left-inverse :
+  rightInverse :
     (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 =
+  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."
+#-}