Codata instances of agda#509

Author: jamesmckinna

CHANGELOG.md

@@ -636,6 +636,12 @@ Deprecated modules
 Deprecated names
 ----------------
 
+* In `Codata.Guarded.Stream.Properties`:
+  ```agda
+  map-identity  ↦  map-id
+  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

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
@@ -309,3 +309,24 @@ 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."
+#-}
+