From 7306dff77b66ae51d71a125bad767fb13b5a238c Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Wed, 5 Jun 2024 10:07:31 -0400
Subject: [PATCH] Very dependent map (#2373)

* add some 'very dependent' maps to Data.Product. More documentation to come later.

* and document

* make imports more precise

* minimal properties of very-dependen map and zipWith. Structured to make it easy to add more.

* whitespace

* implement new names and suggestions about using pattern-matching in the type

* whitespace in CHANGELOG

* small cleanup based on latest round of comments

* and fix the names in the comments too.

---------

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
---
 CHANGELOG.md                               | 17 +++++++
 src/Data/Product.agda                      | 30 ++++++++++--
 src/Data/Product/Properties/Dependent.agda | 53 ++++++++++++++++++++++
 3 files changed, 95 insertions(+), 5 deletions(-)
 create mode 100644 src/Data/Product/Properties/Dependent.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 7b8ca2683a..94a0fd3263 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -586,6 +586,23 @@ Additions to existing modules
   mapMaybe-↭  : xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys
   ```
 
+* Added some very-dependent map and zipWith to `Data.Product`.
+  ```agda
+  map-Σ : {B : A → Set b} {P : A → Set p} {Q : {x : A} → P x → B x → Set q} →
+   (f : (x : A) → B x) → (∀ {x} → (y : P x) → Q y (f x)) →
+   ((x , y) : Σ A P) → Σ (B x) (Q y)
+
+  map-Σ′ : {B : A → Set b} {P : Set p} {Q : P → Set q} →
+    (f : (x : A) → B x) → ((x : P) → Q x) → ((x , y) : A × P) → B x × Q y
+
+  zipWith : {P : A → Set p} {Q : B → Set q} {R : C → Set r} {S : (x : C) → R x → Set s}
+    (_∙_ : A → B → C) → (_∘_ : ∀ {x y} → P x → Q y → R (x ∙ y)) →
+    (_*_ : (x : C) → (y : R x) → S x y) →
+    ((a , p) : Σ A P) → ((b , q) : Σ B Q) →
+        S (a ∙ b) (p ∘ q)
+
+  ```
+
 * In `Data.Rational.Properties`:
   ```agda
   1≢0 : 1ℚ ≢ 0ℚ
diff --git a/src/Data/Product.agda b/src/Data/Product.agda
index 02bf53a97b..d0f6db0cde 100644
--- a/src/Data/Product.agda
+++ b/src/Data/Product.agda
@@ -8,20 +8,40 @@
 
 module Data.Product where
 
-open import Function.Base
-open import Level
-open import Relation.Nullary.Negation.Core
+open import Level using (Level; _⊔_)
+open import Relation.Nullary.Negation.Core using (¬_)
 
 private
   variable
-    a b c ℓ : Level
-    A B : Set a
+    a b c ℓ p q r s : Level
+    A B C : Set a
 
 ------------------------------------------------------------------------
 -- Definition of dependent products
 
 open import Data.Product.Base public
 
+-- These are here as they are not 'basic' but instead "very dependent",
+-- i.e. the result type depends on the full input 'point' (x , y).
+map-Σ : {B : A → Set b} {P : A → Set p} {Q : {x : A} → P x → B x → Set q} →
+   (f : (x : A) → B x) → (∀ {x} → (y : P x) → Q y (f x)) →
+   ((x , y) : Σ A P) → Σ (B x) (Q y)
+map-Σ f g (x , y) = (f x , g y)
+
+-- This is a "non-dependent" version of map-Σ whereby the input is actually
+-- a pair (i.e. _×_ ) but the output type still depends on the input 'point' (x , y).
+map-Σ′ : {B : A → Set b} {P : Set p} {Q : P → Set q} →
+  (f : (x : A) → B x) → ((x : P) → Q x) → ((x , y) : A × P) → B x × Q y
+map-Σ′ f g (x , y) = (f x , g y)
+
+-- This is a generic zipWith for Σ where different functions are applied to each
+-- component pair, and recombined.
+zipWith : {P : A → Set p} {Q : B → Set q} {R : C → Set r} {S : (x : C) → R x → Set s}
+  (_∙_ : A → B → C) → (_∘_ : ∀ {x y} → P x → Q y → R (x ∙ y)) →
+  (_*_ : (x : C) → (y : R x) → S x y) →
+  ((a , p) : Σ A P) → ((b , q) : Σ B Q) → S (a ∙ b) (p ∘ q)
+zipWith _∙_ _∘_ _*_ (a , p) (b , q) = (a ∙ b) * (p ∘ q)
+
 ------------------------------------------------------------------------
 -- Negation of existential quantifier
 
diff --git a/src/Data/Product/Properties/Dependent.agda b/src/Data/Product/Properties/Dependent.agda
new file mode 100644
index 0000000000..122b4e3f12
--- /dev/null
+++ b/src/Data/Product/Properties/Dependent.agda
@@ -0,0 +1,53 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of 'very dependent' map / zipWith over products
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Product.Properties.Dependent where
+
+open import Data.Product using (Σ; _×_; _,_; map-Σ; map-Σ′; zipWith)
+open import Function.Base using (id; flip)
+open import Level using (Level)
+open import Relation.Binary.PropositionalEquality.Core
+  using (_≡_; _≗_; cong₂; refl)
+
+private
+  variable
+    a b p q r s : Level
+    A B C : Set a
+
+------------------------------------------------------------------------
+-- map-Σ
+
+module _ {B : A → Set b} {P : A → Set p} {Q : {x : A} → P x → B x → Set q} where
+
+  map-Σ-cong : {f g : (x : A) → B x} → {h k : ∀ {x} → (y : P x) → Q y (f x)} →
+     (∀ x → f x ≡ g x) →
+     (∀ {x} → (y : P x) → h y ≡ k y) →
+     (v : Σ A P) → map-Σ f h v ≡ map-Σ g k v
+  map-Σ-cong f≗g h≗k (x , y) = cong₂ _,_ (f≗g x) (h≗k y)
+
+------------------------------------------------------------------------
+-- map-Σ′
+
+module _ {B : A → Set b} {P : Set p} {Q : P → Set q} where
+
+  map-Σ′-cong : {f g : (x : A) → B x} → {h k : (x : P) → Q x} →
+     (∀ x → f x ≡ g x) →
+     ((y : P) → h y ≡ k y) →
+     (v : A × P) → map-Σ′ f h v ≡ map-Σ′ g k v
+  map-Σ′-cong f≗g h≗k (x , y) = cong₂ _,_ (f≗g x) (h≗k y)
+
+------------------------------------------------------------------------
+-- zipWith
+
+module _ {P : A → Set p} {Q : B → Set q} {R : C → Set r} {S : (x : C) → R x → Set s} where
+
+  zipWith-flip : (_∙_ : A → B → C) → (_∘_ : ∀ {x y} → P x → Q y → R (x ∙ y)) →
+    (_*_ : (x : C) → (y : R x) → S x y) →
+    {x : Σ A P} → {y : Σ B Q} →
+    zipWith _∙_ _∘_ _*_ x y ≡ zipWith (flip _∙_) (flip _∘_) _*_ y x
+  zipWith-flip _∙_ _∘_ _*_ = refl