Share the proofs of ×-comm and ⊎-comm of type isomorphisms and add a pairing operation

CHANGELOG.md

@@ -190,6 +190,12 @@ Additions to existing modules
   ^-distribʳ-* : ∀ m n o → (n * o) ^ m ≡ n ^ m * o ^ m
   ```
 
+* In `Data.Product.Properties`:
+  ```agda
+  swap-↔ : (A × B) ↔ (B × A)
+  _,′-↔_ : A ↔ C → B ↔ D → (A × B) ↔ (C × D)
+  ```
+
 * In `Data.Vec.Properties`:
   ```agda
   updateAt-take : (xs : Vec A (m + n)) (i : Fin m) (f : A → A) →

src/Data/Product/Properties.agda

@@ -9,9 +9,9 @@
 module Data.Product.Properties where
 
 open import Axiom.UniquenessOfIdentityProofs using (UIP; module Decidable⇒UIP)
-open import Data.Product.Base using (_,_; Σ; _×_; map; swap; ∃; ∃₂)
+open import Data.Product.Base using (_,_; Σ; _,′_; _×_; map; swap; ∃; ∃₂)
 open import Function.Base using (_∋_; _∘_; id)
-open import Function.Bundles using (_↔_; mk↔ₛ′)
+open import Function.Bundles using (_↔_; mk↔ₛ′; Inverse)
 open import Level using (Level)
 open import Relation.Binary.Definitions using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core
@@ -64,6 +64,9 @@ map-cong f≗g h≗i (x , y) = cong₂ _,_ (f≗g x) (h≗i y)
 swap-involutive : swap {A = A} {B = B} ∘ swap ≗ id
 swap-involutive _ = refl
 
+swap-↔ : (A × B) ↔ (B × A)
+swap-↔ = mk↔ₛ′ swap swap swap-involutive swap-involutive
+
 ------------------------------------------------------------------------
 -- Equality between pairs can be expressed as a pair of equalities
 
@@ -111,3 +114,14 @@ module _ {p₁@(a₁ , b₁) p₂@(a₂ , b₂) : A × B} where
 
   from : (∃₂ λ y x → R x y) → (∃₂ λ x y → R x y)
   from (y , x , Rxy) = (x , y , Rxy)
+
+------------------------------------------------------------------------
+-- Non-dependent product (_×_) preserves type isomorphism (_↔_)
+
+infixr 4 _,′-↔_
+
+_,′-↔_ : A ↔ C → B ↔ D → (A × B) ↔ (C × D)
+i ,′-↔ j = mk↔ₛ′ (map (Inverse.to i) (Inverse.to j))
+                 (map (Inverse.from i) (Inverse.from j))
+                 (λ _ → ×-≡,≡→≡ (Inverse.inverseˡ i refl ,′ Inverse.inverseˡ j refl))
+                 (λ _ → ×-≡,≡→≡ (Inverse.inverseʳ i refl ,′ Inverse.inverseʳ j refl))

src/Function/Related/TypeIsomorphisms.agda

@@ -24,8 +24,10 @@ open import Data.Empty.Polymorphic using (⊥; ⊥-elim)
 open import Data.Product.Base as Product
   using (_×_; Σ; curry; uncurry; _,_; -,_; <_,_>; proj₁; proj₂; ∃₂; ∃; ∃-syntax)
 open import Data.Product.Function.NonDependent.Propositional
+import Data.Product.Properties as Product
 open import Data.Sum.Base as Sum
-open import Data.Sum.Properties using (swap-involutive)
+  using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′)
+import Data.Sum.Properties as Sum
 open import Data.Sum.Function.Propositional using (_⊎-cong_)
 open import Data.Unit.Polymorphic.Base using (⊤)
 open import Level using (Level; Lift; 0ℓ; suc)
@@ -63,7 +65,7 @@ open import Relation.Nullary.Decidable public
 -- × is commutative
 
 ×-comm : ∀ (A : Set a) (B : Set b) → (A × B) ↔ (B × A)
-×-comm _ _ = mk↔ₛ′ Product.swap Product.swap (λ _ → refl) λ _ → refl
+×-comm _ _ = Product.swap-↔
 
 -- × has ⊤ as its identity
 
@@ -102,7 +104,7 @@ open import Relation.Nullary.Decidable public
 -- ⊎ is commutative
 
 ⊎-comm : ∀ (A : Set a) (B : Set b) → (A ⊎ B) ↔ (B ⊎ A)
-⊎-comm _ _ = mk↔ₛ′ swap swap swap-involutive swap-involutive
+⊎-comm _ _ = Sum.swap-↔
 
 -- ⊎ has ⊥ as its identity
 
@@ -279,13 +281,7 @@ open import Relation.Nullary.Decidable public
 
 ∃∃↔∃∃ : ∀ {a b p} {A : Set a} {B : Set b} (P : A → B → Set p) →
         (∃₂ λ x y → P x y) ↔ (∃₂ λ y x → P x y)
-∃∃↔∃∃ P = mk↔ₛ′ to from (λ _ → refl) (λ _ → refl)
-  where
-  to : (∃₂ λ x y → P x y) → (∃₂ λ y x → P x y)
-  to (x , y , Pxy) = (y , x , Pxy)
-
-  from : (∃₂ λ y x → P x y) → (∃₂ λ x y → P x y)
-  from (y , x , Pxy) = (x , y , Pxy)
+∃∃↔∃∃ = Product.∃∃↔∃∃
 
 ------------------------------------------------------------------------
 -- Implicit and explicit function spaces are isomorphic