Add Data.Product.Properties.map-cong₂ (#1532)

Author: Taneb

CHANGELOG.md

@@ -123,6 +123,11 @@ Other minor additions
   ```
   and their corresponding algebraic substructures.
 
+* Added new proof to `Data.Product.Properties`:
+  ```agda
+  map-cong : f ≗ g → h ≗ i → map f h ≗ map g i
+  ```
+
 * Added new proofs in `Data.String.Properties`:
   ```
   ≤-isDecTotalOrder-≈ : IsDecTotalOrder _≈_ _≤_

src/Codata/M/Properties.agda

@@ -16,7 +16,7 @@ open import Codata.M.Bisimilarity
 open import Data.Container.Core as C hiding (map)
 import Data.Container.Morphism as Mp
 open import Data.Product as Prod using (_,_)
-open import Data.Product.Properties
+open import Data.Product.Properties hiding (map-cong)
 open import Function
 import Relation.Binary.PropositionalEquality as P
 

src/Data/Product/Properties.agda

@@ -20,9 +20,11 @@ open import Relation.Nullary using (Dec; yes; no)
 
 private
   variable
-    a b ℓ : Level
+    a b c d ℓ : Level
     A : Set a
     B : Set b
+    C : Set c
+    D : Set d
 
 ------------------------------------------------------------------------
 -- Equality (dependent)
@@ -53,6 +55,9 @@ module _ {B : A → Set b} where
 ,-injective : ∀ {a c : A} {b d : B} → (a , b) ≡ (c , d) → a ≡ c × b ≡ d
 ,-injective refl = refl , refl
 
+map-cong : ∀ {f g : A → C} {h i : B → D} → f ≗ g → h ≗ i → map f h ≗ map g i
+map-cong f≗g h≗i (x , y) = cong₂ _,_ (f≗g x) (h≗i y)
+
 -- The following properties are definitionally true (because of η)
 -- but for symmetry with ⊎ it is convenient to define and name them.