Add map⁻ to Unique (#2742)

* Add `map⁻` to `Unique`

* Update src/Data/List/Relation/Unary/AllPairs/Properties.agda

Co-authored-by: jamesmckinna <[email protected]>

* Update `CHANGELOG.md`

* Fix bug by bringing `_on_` into scope

* backport use of `_on_`

* fix: whitespace

* [ fix ] functions are always congruent wrt propeq

* fix: removed redundant `import`

---------

Co-authored-by: jamesmckinna <[email protected]>
Co-authored-by: jamesmckinna <[email protected]>
Co-authored-by: Guillaume Allais <[email protected]>

Author: 3 people

CHANGELOG.md

@@ -327,4 +327,18 @@ Additions to existing modules
   ```agda
   ⊤-reflects : Reflects (⊤ {a}) true
   ⊥-reflects : Reflects (⊥ {a}) false
+
+* In `Data.List.Relation.Unary.AllPairs.Properties`:
+  ```agda
+  map⁻ : AllPairs R (map f xs) → AllPairs (R on f) xs
+  ```
+
+* In `Data.List.Relation.Unary.Unique.Setoid.Properties`:
+  ```agda
+  map⁻ : Congruent _≈₁_ _≈₂_ f → Unique R (map f xs) → Unique S xs
+  ```
+
+* In `Data.List.Relation.Unary.Unique.Propositional.Properties`:
+  ```agda
+  map⁻ : Unique (map f xs) → Unique xs
   ```

src/Data/List/Relation/Unary/AllPairs/Properties.agda

@@ -20,7 +20,7 @@ open import Data.Fin.Base as F using (Fin)
 open import Data.Fin.Properties using (suc-injective; <⇒≢)
 open import Data.Nat.Base using (zero; suc; _<_; z≤n; s≤s; z<s; s<s)
 open import Data.Nat.Properties using (≤-refl; m<n⇒m<1+n)
-open import Function.Base using (_∘_; flip)
+open import Function.Base using (_∘_; flip; _on_)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (DecSetoid)
@@ -42,11 +42,14 @@ private
 
 module _ {R : Rel A ℓ} {f : B → A} where
 
-  map⁺ : ∀ {xs} → AllPairs (λ x y → R (f x) (f y)) xs →
-         AllPairs R (map f xs)
+  map⁺ : ∀ {xs} → AllPairs (R on f) xs → AllPairs R (map f xs)
   map⁺ []           = []
   map⁺ (x∉xs ∷ xs!) = All.map⁺ x∉xs ∷ map⁺ xs!
 
+  map⁻ : ∀ {xs} → AllPairs R (map f xs) → AllPairs (R on f) xs
+  map⁻ {[]}     _              = []
+  map⁻ {_ ∷ _} (fx∉fxs ∷ fxs!) = All.map⁻ fx∉fxs ∷ map⁻ fxs!
+
 ------------------------------------------------------------------------
 -- ++
 

src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda

@@ -30,7 +30,7 @@ open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.PropositionalEquality.Core
-  using (refl; _≡_; _≢_; sym)
+  using (refl; _≡_; _≢_; sym; cong)
 open import Relation.Binary.PropositionalEquality.Properties using (setoid)
 open import Relation.Unary using (Pred; Decidable)
 open import Relation.Nullary.Negation using (¬_)
@@ -53,6 +53,9 @@ module _ {A : Set a} {B : Set b} where
          ∀ {xs} → Unique xs → Unique (map f xs)
   map⁺ = Setoid.map⁺ (setoid A) (setoid B)
 
+  map⁻ : ∀ {f xs} → Unique (map f xs) → Unique xs
+  map⁻ = Setoid.map⁻ (setoid A) (setoid B) (cong _)
+
 ------------------------------------------------------------------------
 -- ++
 

src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda

@@ -24,6 +24,7 @@ import Data.List.Relation.Unary.AllPairs.Properties as AllPairs
 open import Data.Fin.Base using (Fin)
 open import Data.Nat.Base using (_<_)
 open import Function.Base using (_∘_; id)
+open import Function.Definitions using (Congruent)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (Setoid)
@@ -50,6 +51,10 @@ module _ (S : Setoid a ℓ₁) (R : Setoid b ℓ₂) where
          ∀ {xs} → Unique S xs → Unique R (map f xs)
   map⁺ inj xs! = AllPairs.map⁺ (AllPairs.map (contraposition inj) xs!)
 
+  map⁻ : ∀ {f} → Congruent _≈₁_ _≈₂_ f →
+         ∀ {xs} → Unique R (map f xs) → Unique S xs
+  map⁻ cong fxs! = AllPairs.map (contraposition cong) (AllPairs.map⁻ fxs!)
+
 ------------------------------------------------------------------------
 -- ++