[ fix #1694 ] Add ordered algebraic structures.

Author: sstucki

CHANGELOG.md

@@ -800,6 +800,14 @@ New modules
   Algebra.Morphism.Construct.Identity
   ```
 
+* Ordered algebraic structures (pomonoids, posemigroups, etc.)
+  ```
+  Algebra.Ordered
+  Algebra.Ordered.Bundles
+  Algebra.Ordered.Definitions
+  Algebra.Ordered.Structures
+  ```
+
 * 'Optimised' tail-recursive exponentiation properties:
   ```
   Algebra.Properties.Semiring.Exp.TailRecursiveOptimised
@@ -1549,10 +1557,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 _≈_
@@ -1666,6 +1682,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 +1964,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,15 @@
+------------------------------------------------------------------------
+-- 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.Definitions public
+open import Algebra.Ordered.Structures public
+open import Algebra.Ordered.Bundles public