Add CHANGELOG and slightly simpler definition

Author: WhatisRT

CHANGELOG.md

@@ -71,6 +71,11 @@ Additions to existing modules
   ++⁺ˡ : Reflexive R → ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R)
   ```
 
+* In `Data.Maybe.Properties`:
+  ```agda
+  maybe′-∘ : ∀ {b} (f : B → C) (g : A → B) → f ∘ (maybe′ g b) ≗ maybe′ (f ∘ g) (f b)
+  ```
+
 * New lemmas in `Data.Nat.Properties`:
   ```agda
   m≤n⇒m≤n*o : ∀ o .{{_ : NonZero o}} → m ≤ n → m ≤ n * o

src/Data/Maybe/Properties.agda

@@ -97,9 +97,8 @@ maybe′-map : ∀ j (n : C) (f : A → B) ma →
              maybe′ j n (map f ma) ≡ maybe′ (j ∘′ f) n ma
 maybe′-map = maybe-map
 
-maybe-∘ : ∀ {c x} (f : B → C) (g : A → B) → f (maybe g c x) ≡ maybe (f ∘ g) (f c) x
-maybe-∘ {x = just _}  _ _ = refl
-maybe-∘ {x = nothing} _ _ = refl
+maybe′-∘ : ∀ {b} (f : B → C) (g : A → B) → f ∘ (maybe′ g b) ≗ maybe′ (f ∘ g) (f b)
+maybe′-∘ _ _ = maybe (λ _ → refl) refl
 
 ------------------------------------------------------------------------
 -- _<∣>_