Add properties relating upTo/downFrom and map (#2590)

Author: Taneb

CHANGELOG.md

@@ -32,7 +32,7 @@ Deprecated names
   _∤∤_    ↦  _∦_
   ```
 
-* In `Algebra.Module.Consequences
+* In `Algebra.Module.Consequences`
   ```agda
   *ₗ-assoc+comm⇒*ᵣ-assoc      ↦  *ₗ-assoc∧comm⇒*ᵣ-assoc
   *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc   ↦  *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc
@@ -126,3 +126,10 @@ Additions to existing modules
   quasiring                       : Quasiring c ℓ → Quasiring (a ⊔ c) (a ⊔ ℓ)
   commutativeRing                 : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ)
   ```
+* In `Data.List.Properties`:
+  ```agda
+  map-applyUpTo : ∀ (f : ℕ → A) (g : A → B) n → map g (applyUpTo f n) ≡ applyUpTo (g ∘ f) n
+  map-applyDownFrom : ∀ (f : ℕ → A) (g : A → B) n → map g (applyDownFrom f n) ≡ applyDownFrom (g ∘ f) n
+  map-upTo : ∀ (f : ℕ → A) n → map f (upTo n) ≡ applyUpTo f n
+  map-downFrom : ∀ (f : ℕ → A) n → map f (downFrom n) ≡ applyDownFrom f n
+  ```

src/Data/List/Properties.agda

@@ -842,6 +842,10 @@ applyUpTo-∷ʳ : ∀ (f : ℕ → A) n → applyUpTo f n ∷ʳ f n ≡ applyUpT
 applyUpTo-∷ʳ f zero = refl
 applyUpTo-∷ʳ f (suc n) = cong (f 0 ∷_) (applyUpTo-∷ʳ (f ∘ suc) n)
 
+map-applyUpTo : ∀ (f : ℕ → A) (g : A → B) n → map g (applyUpTo f n) ≡ applyUpTo (g ∘ f) n
+map-applyUpTo f g zero = refl
+map-applyUpTo f g (suc n) = cong (g (f 0) ∷_) (map-applyUpTo (f ∘ suc) g n)
+
 ------------------------------------------------------------------------
 -- applyDownFrom
 
@@ -859,6 +863,10 @@ module _ (f : ℕ → A) where
   applyDownFrom-∷ʳ zero = refl
   applyDownFrom-∷ʳ (suc n) = cong (f (suc n) ∷_) (applyDownFrom-∷ʳ n)
 
+  map-applyDownFrom : ∀ (g : A → B) n → map g (applyDownFrom f n) ≡ applyDownFrom (g ∘ f) n
+  map-applyDownFrom g zero = refl
+  map-applyDownFrom g (suc n) = cong (g (f n) ∷_) (map-applyDownFrom g n)
+
 ------------------------------------------------------------------------
 -- upTo
 
@@ -871,6 +879,9 @@ lookup-upTo = lookup-applyUpTo id
 upTo-∷ʳ : ∀ n → upTo n ∷ʳ n ≡ upTo (suc n)
 upTo-∷ʳ = applyUpTo-∷ʳ id
 
+map-upTo : ∀ (f : ℕ → A) n → map f (upTo n) ≡ applyUpTo f n
+map-upTo = map-applyUpTo id
+
 ------------------------------------------------------------------------
 -- downFrom
 
@@ -883,6 +894,9 @@ lookup-downFrom = lookup-applyDownFrom id
 downFrom-∷ʳ : ∀ n → applyDownFrom suc n ∷ʳ 0 ≡ downFrom (suc n)
 downFrom-∷ʳ = applyDownFrom-∷ʳ id
 
+map-downFrom : ∀ (f : ℕ → A) n → map f (downFrom n) ≡ applyDownFrom f n
+map-downFrom = map-applyDownFrom id
+
 ------------------------------------------------------------------------
 -- tabulate