Resolves issue #509 and resolves issue #626

CHANGELOG.md

@@ -685,6 +685,42 @@ Deprecated modules
 Deprecated names
 ----------------
 
+* In `Codata.Guarded.Stream.Properties`:
+  ```agda
+  map-identity  ↦  map-id
+  map-fusion    ↦  map-∘
+  ```
+
+* In `Codata.Sized.Colist.Properties`:
+  ```agda
+  map-identity   ↦  map-id
+  map-map-fusion  ↦  map-∘
+  ```
+
+* In `Codata.Sized.Covec.Properties`:
+  ```agda
+  map-identity   ↦  map-id
+  map-map-fusion  ↦  map-∘
+  ```
+
+* In `Codata.Sized.Delay.Properties`:
+  ```agda
+  map-identity      ↦  map-id
+  map-map-fusion    ↦  map-∘
+  map-unfold-fusion  ↦  map-unfold
+  ```
+
+* In `Codata.Sized.M.Properties`:
+  ```agda
+  map-compose  ↦  map-∘
+  ```
+
+* In `Codata.Sized.Stream.Properties`:
+  ```agda
+  map-identity   ↦  map-id
+  map-map-fusion  ↦  map-∘
+  ```
+
 * In `Data.Fin.Base`: two new, hopefully more memorable, names `↑ˡ` `↑ʳ`
   for the 'left', resp. 'right' injection of a Fin m into a 'larger' type,
   `Fin (m + n)`, resp. `Fin (n + m)`, with argument order to reflect the
@@ -768,10 +804,52 @@ Deprecated names
 
 * In `Data.List.Properties`:
   ```agda
+  map-id₂         ↦  map-id-local
+  map-cong₂       ↦  map-cong-local
+  map-compose     ↦  map-∘
+
+  map-++-commute       ↦  map-++
+  sum-++-commute       ↦  sum-++
+  reverse-map-commute  ↦  reverse-map
+  reverse-++-commute   ↦  reverse-++
+
   zipWith-identityˡ  ↦  zipWith-zeroˡ
   zipWith-identityʳ  ↦  zipWith-zeroʳ
   ```
 
+* In `Data.List.NonEmpty.Properties`:
+  ```agda
+  map-compose     ↦  map-∘
+
+  map-++⁺-commute ↦  map-++⁺
+  ```
+
+* In `Data.List.Relation.Unary.All.Properties`:
+  ```agda
+  updateAt-id-relative      ↦  updateAt-id-local
+  updateAt-compose-relative ↦  updateAt-∘-local
+  updateAt-compose          ↦  updateAt-∘
+  updateAt-cong-relative    ↦  updateAt-cong-local
+  ```
+
+* In `Data.List.Zipper.Properties`:
+  ```agda
+  toList-reverse-commute ↦  toList-reverse
+  toList-ˡ++-commute     ↦  toList-ˡ++
+  toList-++ʳ-commute     ↦  toList-++ʳ
+  toList-map-commute    ↦  toList-map
+  toList-foldr-commute  ↦  toList-foldr
+  ```
+
+* In `Data.Maybe.Properties`:
+  ```agda
+  map-id₂     ↦  map-id-local
+  map-cong₂   ↦  map-cong-local
+
+  map-compose    ↦  map-∘
+
+  map-<∣>-commute ↦  map-<∣>
+
 * In `Data.List.Relation.Binary.Subset.Propositional.Properties`:
   ```
   map-with-∈⁺  ↦  mapWith∈⁺
@@ -819,8 +897,38 @@ Deprecated names
   negative<positive     ↦ neg<pos
   ```
 
+* In `Data.Sum.Properties`:
+  ```agda
+  [,]-∘-distr      ↦  [,]-∘
+  [,]-map-commute  ↦  [,]-map
+  map-commute      ↦  map-map
+  map₁₂-commute    ↦  map₁₂-map₂₁
+  ```
+
+* In `Data.Tree.Binary.Zipper.Properties`:
+  ```
+  toTree-#nodes-commute   ↦  toTree-#nodes
+  toTree-#leaves-commute  ↦  toTree-#leaves
+  toTree-map-commute      ↦  toTree-map
+  toTree-foldr-commute    ↦  toTree-foldr
+  toTree-⟪⟫ˡ-commute      ↦  toTree--⟪⟫ˡ
+  toTree-⟪⟫ʳ-commute      ↦  toTree-⟪⟫ʳ
+  ```
+
+* In `Data.Tree.Rose.Properties`:
+  ```agda
+  map-compose     ↦  map-∘
+  ```
+
 * In `Data.Vec.Properties`:
   ```
+  updateAt-id-relative      ↦  updateAt-id-local
+  updateAt-compose-relative ↦  updateAt-∘-local
+  updateAt-compose          ↦  updateAt-∘
+  updateAt-cong-relative    ↦  updateAt-cong-local
+
+  []%=-compose    ↦  []%=-∘
+
   []≔-++-inject+  ↦ []≔-++-↑ˡ
   []≔-++-raise    ↦ []≔-++-↑ʳ
   idIsFold        ↦ id-is-foldr
@@ -835,6 +943,27 @@ Deprecated names
   zipWith-comm : ∀ {f : A → B → C} {g : B → A → C}  (comm : ∀ x y → f x y ≡ g y x) (xs : Vec A n) ys → zipWith f xs ys ≡ zipWith g ys xs
   ```
 
+* In `Data.Vec.Functional.Properties`:
+  ```
+  updateAt-id-relative      ↦  updateAt-id-local
+  updateAt-compose-relative ↦  updateAt-∘-local
+  updateAt-compose          ↦  updateAt-∘
+  updateAt-cong-relative    ↦  updateAt-cong-local
+
+  map-updateAt              ↦  map-updateAt-local
+  ```
+  NB. This last one is complicated by the *addition* of a 'global' property `map-updateAt`
+
+* In `Data.Vec.Recursive.Properties`:
+  ```
+  append-cons-commute  ↦  append-cons
+  ```
+
+* In `Data.Vec.Relation.Binary.Equality.Setoid`:
+  ```agda
+  map-++-commute ↦  map-++
+  ```
+
 * In `Function.Construct.Composition`:
   ```
   _∘-⟶_   ↦   _⟶-∘_
@@ -1725,6 +1854,11 @@ Other minor changes
   transpose-replicate : transpose (replicate xs) ≡ map replicate xs
   ```
 
+* Added new proofs in `Data.Vec.Functional.Properties`:
+  ```
+  map-updateAt : f ∘ g ≗ h ∘ f → map f (updateAt i g xs) ≗ updateAt i h (map f xs)
+  ```
+
 * Added new proofs in `Data.Vec.Relation.Binary.Lex.Strict`:
   ```agda
   xs≮[] : ∀ {n} (xs : Vec A n) → ¬ xs < []

src/Codata/Guarded/Stream/Properties.agda

@@ -134,13 +134,13 @@ map-const : (a : A) (bs : Stream B) → map (const a) bs ≈ repeat a
 map-const a bs .head = P.refl
 map-const a bs .tail = map-const a (bs .tail)
 
-map-identity : (as : Stream A) → map id as ≈ as
-map-identity as .head = P.refl
-map-identity as .tail = map-identity (as .tail)
+map-id : (as : Stream A) → map id as ≈ as
+map-id as .head = P.refl
+map-id as .tail = map-id (as .tail)
 
-map-fusion : ∀ (g : B → C) (f : A → B) as → map g (map f as) ≈ map (g ∘′ f) as
-map-fusion g f as .head = P.refl
-map-fusion g f as .tail = map-fusion g f (as .tail)
+map-∘ : ∀ (g : B → C) (f : A → B) as → map g (map f as) ≈ map (g ∘′ f) as
+map-∘ g f as .head = P.refl
+map-∘ g f as .tail = map-∘ g f (as .tail)
 
 map-unfold : ∀ (g : B → C) (f : A → A × B) a →
              map g (unfold f a) ≈ unfold (Prod.map₂ g ∘′ f) a
@@ -311,3 +311,23 @@ interleave-evens-odds : (as : Stream A) → interleave (evens as) (odds as) ≈
 interleave-evens-odds as .head       = P.refl
 interleave-evens-odds as .tail .head = P.refl
 interleave-evens-odds as .tail .tail = interleave-evens-odds (as .tail .tail)
+
+------------------------------------------------------------------------
+-- DEPRECATED
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.0
+
+map-identity = map-id
+{-# WARNING_ON_USAGE map-identity
+"Warning: map-identity was deprecated in v2.0.
+Please use map-id instead."
+#-}
+
+map-fusion = map-∘
+{-# WARNING_ON_USAGE map-fusion
+"Warning: map-fusion was deprecated in v2.0.
+Please use map-∘ instead."
+#-}

src/Codata/Sized/Colist/Properties.agda

@@ -45,15 +45,15 @@ private
 ------------------------------------------------------------------------
 -- Functor laws
 
-map-identity : ∀ (as : Colist A ∞) → i ⊢ map id as ≈ as
-map-identity []       = []
-map-identity (a ∷ as) = Eq.refl ∷ λ where .force → map-identity (as .force)
+map-id : ∀ (as : Colist A ∞) → i ⊢ map id as ≈ as
+map-id []       = []
+map-id (a ∷ as) = Eq.refl ∷ λ where .force → map-id (as .force)
 
-map-map-fusion : ∀ (f : A → B) (g : B → C) as {i} →
+map-∘ : ∀ (f : A → B) (g : B → C) as {i} →
                  i ⊢ map g (map f as) ≈ map (g ∘ f) as
-map-map-fusion f g []       = []
-map-map-fusion f g (a ∷ as) =
-  Eq.refl ∷ λ where .force → map-map-fusion f g (as .force)
+map-∘ f g []       = []
+map-∘ f g (a ∷ as) =
+  Eq.refl ∷ λ where .force → map-∘ f g (as .force)
 
 ------------------------------------------------------------------------
 -- Relation to Cowriter
@@ -161,8 +161,8 @@ module _ (cons : C → B → C) (alg : A → Maybe (A × B)) where
 
 map-alignWith : ∀ (f : C → D) (al : These A B → C) as bs →
                 i ⊢ map f (alignWith al as bs) ≈ alignWith (f ∘ al) as bs
-map-alignWith f al []         bs       = map-map-fusion (al ∘′ that) f bs
-map-alignWith f al as@(_ ∷ _) []       = map-map-fusion (al ∘′ this) f as
+map-alignWith f al []         bs       = map-∘ (al ∘′ that) f bs
+map-alignWith f al as@(_ ∷ _) []       = map-∘ (al ∘′ this) f as
 map-alignWith f al (a ∷ as)   (b ∷ bs) =
   Eq.refl ∷ λ where .force → map-alignWith f al (as .force) (bs .force)
 
@@ -331,3 +331,23 @@ map-fromStream : ∀ (f : A → B) as →
                  i ⊢ map f (fromStream as) ≈ fromStream (Stream.map f as)
 map-fromStream f (a ∷ as) =
   Eq.refl ∷ λ where .force → map-fromStream f (as .force)
+
+------------------------------------------------------------------------
+-- DEPRECATED
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.0
+
+map-identity = map-id
+{-# WARNING_ON_USAGE map-identity
+"Warning: map-identity was deprecated in v2.0.
+Please use map-id instead."
+#-}
+
+map-map-fusion = map-∘
+{-# WARNING_ON_USAGE map-map-fusion
+"Warning: map-map-fusion was deprecated in v2.0.
+Please use map-∘ instead."
+#-}

src/Codata/Sized/Covec/Properties.agda

@@ -20,12 +20,32 @@ open import Relation.Binary.PropositionalEquality as Eq
 
 module _ {a} {A : Set a} where
 
- map-identity : ∀ {m} (as : Covec A ∞ m) {i} → i , m ⊢ map id as ≈ as
- map-identity []       = []
- map-identity (a ∷ as) = Eq.refl ∷ λ where .force → map-identity (as .force)
+ map-id : ∀ {m} (as : Covec A ∞ m) {i} → i , m ⊢ map id as ≈ as
+ map-id []       = []
+ map-id (a ∷ as) = Eq.refl ∷ λ where .force → map-id (as .force)
 
 module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where
 
- map-map-fusion : ∀ (f : A → B) (g : B → C) {m} as {i} → i , m ⊢ map g (map f as) ≈ map (g ∘ f) as
- map-map-fusion f g []       = []
- map-map-fusion f g (a ∷ as) = Eq.refl ∷ λ where .force → map-map-fusion f g (as .force)
+ map-∘ : ∀ (f : A → B) (g : B → C) {m} as {i} → i , m ⊢ map g (map f as) ≈ map (g ∘ f) as
+ map-∘ f g []       = []
+ map-∘ f g (a ∷ as) = Eq.refl ∷ λ where .force → map-∘ f g (as .force)
+
+------------------------------------------------------------------------
+-- DEPRECATED
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.0
+
+map-identity = map-id
+{-# WARNING_ON_USAGE map-identity
+"Warning: map-identity was deprecated in v2.0.
+Please use map-id instead."
+#-}
+
+map-map-fusion = map-∘
+{-# WARNING_ON_USAGE map-map-fusion
+"Warning: map-map-fusion was deprecated in v2.0.
+Please use map-∘ instead."
+#-}

src/Codata/Sized/Delay/Properties.agda

@@ -39,16 +39,20 @@ module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where
  length-zipWith f (later da)   (later db) =
    suc λ where .force →  length-zipWith f (da .force) (db .force)
 
- map-map-fusion : ∀ (f : A → B) (g : B → C) da {i}  →
+ map-id : ∀ da {i} → i ⊢ map (id {A = A}) da ≈ da
+ map-id (now a)    = now Eq.refl
+ map-id (later da) = later λ where .force → map-id (da .force)
+
+ map-∘ : ∀ (f : A → B) (g : B → C) da {i}  →
    i ⊢ map g (map f da) ≈ map (g ∘′ f) da
- map-map-fusion f g (now a)    = now Eq.refl
- map-map-fusion f g (later da) = later λ where .force → map-map-fusion f g (da .force)
+ map-∘ f g (now a)    = now Eq.refl
+ map-∘ f g (later da) = later λ where .force → map-∘ f g (da .force)
 
- map-unfold-fusion : ∀ (f : B → C) n (s : A) {i} →
+ map-unfold : ∀ (f : B → C) n (s : A) {i} →
    i ⊢ map f (unfold n s) ≈ unfold (Sum.map id f ∘′ n) s
- map-unfold-fusion f n s with n s
- ... | Sum.inj₁ s′ = later λ where .force → map-unfold-fusion f n s′
- ... | Sum.inj₂ b  = now Eq.refl
+ map-unfold f n s with n s
+ ... | Sum.inj₁ s′ = later λ where .force → map-unfold f n s′
+ ... | Sum.inj₂ b = now Eq.refl
 
 
 ------------------------------------------------------------------------
@@ -105,3 +109,29 @@ module _ {a} {A B : Set a} where
     Eq.cong (toℕ ∘′ length-⇓) (⇓-unique bind⇓ f⇓)
   bind⇓-length {d = d@(later dt)} {f = f} bind⇓@(later bind'⇓) d⇓@(later r) f⇓ =
     Eq.cong ℕ.suc (bind⇓-length bind'⇓ r f⇓)
+
+------------------------------------------------------------------------
+-- DEPRECATED
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.0
+
+map-identity = map-id
+{-# WARNING_ON_USAGE map-identity
+"Warning: map-identity was deprecated in v2.0.
+Please use map-id instead."
+#-}
+
+map-map-fusion = map-∘
+{-# WARNING_ON_USAGE map-map-fusion
+"Warning: map-map-fusion was deprecated in v2.0.
+Please use map-∘ instead."
+#-}
+
+map-unfold-fusion = map-unfold
+{-# WARNING_ON_USAGE map-unfold-fusion
+"Warning: map-unfold-fusion was deprecated in v2.0.
+Please use map-unfold instead."
+#-}