Merge branch 'master' into solver-refactor

CHANGELOG.md

@@ -24,6 +24,12 @@ Deprecated modules
 Deprecated names
 ----------------
 
+* In `Algebra.Properties.CommutativeMagma.Divisibility`:
+  ```agda
+  ∣-factors    ↦  x|xy∧y|xy
+  ∣-factors-≈  ↦  xy≈z⇒x|z∧y|z
+  ```
+
 * In `Algebra.Solver.CommutativeMonoid`:
   ```agda
   normalise-correct  ↦  Algebra.Solver.CommutativeMonoid.Normal.correct
@@ -112,6 +118,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

src/Algebra/Properties/CommutativeMagma/Divisibility.agda

@@ -7,15 +7,14 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra using (CommutativeMagma)
-open import Data.Product.Base using (_×_; _,_; map)
 
 module Algebra.Properties.CommutativeMagma.Divisibility
   {a ℓ} (CM : CommutativeMagma a ℓ)
   where
 
-open CommutativeMagma CM
+open import Data.Product.Base using (_×_; _,_)
 
-open import Relation.Binary.Reasoning.Setoid setoid
+open CommutativeMagma CM using (magma; _≈_; _∙_; comm)
 
 ------------------------------------------------------------------------
 -- Re-export the contents of magmas
@@ -31,8 +30,28 @@ x∣xy x y = y , comm y x
 xy≈z⇒x∣z : ∀ x y {z} → x ∙ y ≈ z → x ∣ z
 xy≈z⇒x∣z x y xy≈z = ∣-respʳ xy≈z (x∣xy x y)
 
-∣-factors : ∀ x y → (x ∣ x ∙ y) × (y ∣ x ∙ y)
-∣-factors x y = x∣xy x y , x∣yx y x
+x|xy∧y|xy : ∀ x y → (x ∣ x ∙ y) × (y ∣ x ∙ y)
+x|xy∧y|xy x y = x∣xy x y , x∣yx y x
 
-∣-factors-≈ : ∀ x y {z} → x ∙ y ≈ z → x ∣ z × y ∣ z
-∣-factors-≈ x y xy≈z = xy≈z⇒x∣z x y xy≈z , xy≈z⇒y∣z x y xy≈z
+xy≈z⇒x|z∧y|z : ∀ x y {z} → x ∙ y ≈ z → x ∣ z × y ∣ z
+xy≈z⇒x|z∧y|z x y xy≈z = xy≈z⇒x∣z x y xy≈z , xy≈z⇒y∣z x y xy≈z
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.2
+
+∣-factors = x|xy∧y|xy
+{-# WARNING_ON_USAGE ∣-factors
+"Warning: ∣-factors was deprecated in v2.2.
+Please use x|xy∧y|xy instead. "
+#-}
+∣-factors-≈ = xy≈z⇒x|z∧y|z
+{-# WARNING_ON_USAGE ∣-factors-≈
+"Warning: ∣-factors-≈ was deprecated in v2.2.
+Please use xy≈z⇒x|z∧y|z instead. "
+#-}

src/Data/List/Relation/Unary/All.agda

@@ -115,7 +115,7 @@ zip = zipWith id
 unzip : All (P ∩ Q) ⊆ All P ∩ All Q
 unzip = unzipWith id
 
-module _(S : Setoid a ℓ) {P : Pred (Setoid.Carrier S) p} where
+module _ (S : Setoid a ℓ) {P : Pred (Setoid.Carrier S) p} where
   open Setoid S renaming (refl to ≈-refl)
   open SetoidMembership S
 

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
+
 ------------------------------------------------------------------------
 -- _<∣>_