[ fix #1694 ] Add ordered algebraic structures.

CHANGELOG.md

@@ -800,6 +800,13 @@ New modules
   Algebra.Morphism.Construct.Identity
   ```
 
+* Ordered algebraic structures (pomonoids, posemigroups, etc.)
+  ```
+  Algebra.Ordered
+  Algebra.Ordered.Bundles
+  Algebra.Ordered.Structures
+  ```
+
 * 'Optimised' tail-recursive exponentiation properties:
   ```
   Algebra.Properties.Semiring.Exp.TailRecursiveOptimised
@@ -1549,10 +1556,18 @@ Other minor changes
 
 * Added new proofs to `Relation.Binary.Lattice.Properties.{Join,Meet}Semilattice`:
   ```agda
+  isPosemigroup : IsPosemigroup _≈_ _≤_ _∨_
+  posemigroup : Posemigroup c ℓ₁ ℓ₂
   ≈-dec⇒≤-dec : Decidable _≈_ → Decidable _≤_
   ≈-dec⇒isDecPartialOrder : Decidable _≈_ → IsDecPartialOrder _≈_ _≤_
   ```
 
+* Added new proofs to `Relation.Binary.Lattice.Properties.Bounded{Join,Meet}Semilattice`:
+  ```agda
+  isCommutativePomonoid : IsCommutativePomonoid _≈_ _≤_ _∨_ ⊥
+  commutativePomonoid : CommutativePomonoid c ℓ₁ ℓ₂
+  ```
+
 * Added new proofs to `Relation.Binary.Properties.Poset`:
   ```agda
   ≤-dec⇒≈-dec : Decidable _≤_ → Decidable _≈_
@@ -1649,6 +1664,14 @@ Other minor changes
   ```
   Cotransitive _#_ = ∀ {x y} → x # y → ∀ z → (x # z) ⊎ (z # y)
   Tight    _≈_ _#_ = ∀ x y → (¬ x # y → x ≈ y) × (x ≈ y → ¬ x # y)
+
+  Monotonic₁         _≤_ _⊑_ f     = f Preserves _≤_ ⟶ _⊑_
+  Antitonic₁         _≤_ _⊑_ f     = f Preserves (flip _≤_) ⟶ _⊑_
+  Monotonic₂         _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ _≤_ ⟶ _⊑_ ⟶ _≼_
+  MonotonicAntitonic _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ _≤_ ⟶ (flip _⊑_) ⟶ _≼_
+  AntitonicMonotonic _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ (flip _≤_) ⟶ _⊑_ ⟶ _≼_
+  Antitonic₂         _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ (flip _≤_) ⟶ (flip _⊑_) ⟶ _≼_
+  Adjoint            _≤_ _⊑_ f g   = ∀ {x y} → (f x ⊑ y → x ≤ g y) × (x ≤ g y → f x ⊑ y)
   ```
 
 * Added new definitions in `Relation.Binary.Bundles`:
@@ -1666,6 +1689,9 @@ Other minor changes
   sym⇒¬-sym       : Symmetric _∼_ → Symmetric _≁_
   cotrans⇒¬-trans : Cotransitive _∼_ → Transitive _≁_
   irrefl⇒¬-refl   : Reflexive _≈_ → Irreflexive _≈_ _∼_ →  Reflexive _≁_
+  mono₂⇒cong₂     : Symmetric ≈₁ → ≈₁ ⇒ ≤₁ → Antisymmetric ≈₂ ≤₂ → ∀ {f} →
+                    f Preserves₂ ≤₁ ⟶ ≤₁ ⟶ ≤₂ →
+                    f Preserves₂ ≈₁ ⟶ ≈₁ ⟶ ≈₂
   ```
 
 * Added new operations in `Relation.Binary.PropositionalEquality.Properties`:
@@ -1945,4 +1971,4 @@ This is a full list of proofs that have changed form to use irrelevant instance
   ```agda
   Inverse⇒Injection : Inverse S T → Injection S T
   ↔⇒↣ : A ↔ B → A ↣ B
-  ```
+  ```

src/Algebra/Ordered.agda

@@ -0,0 +1,14 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definitions of ordered algebraic structures like promonoids and
+-- posemigroups (packed in records together with sets, orders,
+-- operations, etc.)
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Algebra.Ordered where
+
+open import Algebra.Ordered.Structures public
+open import Algebra.Ordered.Bundles public