Add a property relating maybe to composition (#2414)

* Add a property relating `maybe` to composition * Add CHANGELOG and slightly simpler definition * Update CHANGELOG.md Co-authored-by: jamesmckinna <[email protected]> --------- Co-authored-by: Jacques Carette <[email protected]> Co-authored-by: jamesmckinna <[email protected]>
agda · Sep 1, 2024 · 6faaad3 · 6faaad3
1 parent cc69ea0
commit 6faaad3
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git a/CHANGELOG.md b/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′-∘ : ∀ f g → 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

diff --git a/src/Data/Maybe/Properties.agda b/src/Data/Maybe/Properties.agda
@@ -97,6 +97,9 @@ 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′-∘ : ∀ {b} (f : B → C) (g : A → B) → f ∘ (maybe′ g b) ≗ maybe′ (f ∘ g) (f b)
+maybe′-∘ _ _ = maybe (λ _ → refl) refl
+
 ------------------------------------------------------------------------
 -- _<∣>_