Add sum-↭ (#2498)

Author: Taneb

CHANGELOG.md

@@ -111,6 +111,9 @@ New modules
 
 * `Data.List.Relation.Binary.Disjoint.Propositional.Properties`:
   Propositional counterpart to `Data.List.Relation.Binary.Disjoint.Setoid.Properties`
+  ```agda
+  sum-↭ : sum Preserves _↭_ ⟶ _≡_
+  ```
 
 * `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`
 

src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda

@@ -372,6 +372,15 @@ module _ {ℓ} {R : Rel A ℓ} (R? : Decidable R) where
     x ∷ xs ++ y ∷ ys         ∎
     where open PermutationReasoning
 
+------------------------------------------------------------------------
+-- sum
+
+sum-↭ : sum Preserves _↭_ ⟶ _≡_
+sum-↭ p = foldr-commMonoid ℕ-+-0.isCommutativeMonoid (↭⇒↭ₛ p)
+  where
+  module ℕ-+-0 = CommutativeMonoid ℕ.+-0-commutativeMonoid
+  open Permutation ℕ-+-0.setoid
+
 ------------------------------------------------------------------------
 -- product