Add an Inverse for swap in module Data.Sum.Properties (#1720)

Author: sseefried

CHANGELOG.md

@@ -1237,6 +1237,10 @@ Other minor changes
   ≤-isDecTotalOrder-≈ : IsDecTotalOrder _≈_ _≤_
   ≤-decTotalOrder-≈   :  DecTotalOrder _ _ _
   ```
+* Added new definitions in `Data.Sum.Properties`:
+  ```
+  swap-↔ : (A ⊎ B) ↔ (B ⊎ A)
+  ```
 
 * Added new proofs in `Data.Sum.Properties`:
   ```

src/Data/Sum/Properties.agda

@@ -11,11 +11,13 @@ module Data.Sum.Properties where
 open import Level
 open import Data.Sum.Base
 open import Function
+open import Function.Bundles using (mk↔′)
 open import Relation.Binary using (Decidable)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary using (yes; no)
 open import Relation.Nullary.Decidable using (map′)
 
+
 private
   variable
     a b c d e f : Level
@@ -44,6 +46,9 @@ module _ (dec₁ : Decidable {A = A} {B = A} _≡_)
 swap-involutive : swap {A = A} {B = B} ∘ swap ≗ id
 swap-involutive = [ (λ _ → refl) , (λ _ → refl) ]
 
+swap-↔ : (A ⊎ B) ↔ (B ⊎ A)
+swap-↔ = mk↔′ swap swap swap-involutive swap-involutive
+
 map-id : map {A = A} {B = B} id id ≗ id
 map-id (inj₁ _) = refl
 map-id (inj₂ _) = refl