    -- | Partially ordered monoids.

    module Agda.Utils.POMonoid where

    import Data.Semigroup
    import Data.Monoid

    import Agda.Utils.PartialOrd

    -- | Partially ordered semigroup.
    --
    -- Law: composition must be monotone.
    --
    -- @
    --   related x POLE x' && related y POLE y' ==>
    --   related (x <> y) POLE (x' <> y')
    -- @

    class (PartialOrd a, Semigroup a) => POSemigroup a where

    -- | Partially ordered monoid.
    --
    -- Law: composition must be monotone.
    --
    -- @
    --   related x POLE x' && related y POLE y' ==>
    --   related (x <> y) POLE (x' <> y')
    -- @

    class (PartialOrd a, Monoid a) => POMonoid a where

    -- | Completing POMonoids with inverses to form a Galois connection.
    --
    -- Law: composition and inverse composition form a Galois connection.
    --
    -- @
    --   related (inverseCompose p x) POLE y <==> related x POLE (p <> y)
    -- @

    class POMonoid a => LeftClosedPOMonoid a where
      inverseCompose :: a -> a -> a