    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | Partially ordered monoids.

    module Agda.Utils.POMonoid where

    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, Semigroup 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

    -- | @hasLeftAdjoint x@ checks whether
    --   @x^-1 := x `inverseCompose` mempty@ is such that
    --   @x `inverseCompose` y == x^-1 <> y@ for any @y@.
    hasLeftAdjoint :: LeftClosedPOMonoid a => a -> Bool
    hasLeftAdjoint :: forall a. LeftClosedPOMonoid a => a -> Bool
    hasLeftAdjoint a
    x = a -> PartialOrdering -> a -> Bool
    forall a. PartialOrd a => a -> PartialOrdering -> a -> Bool
    related (a -> a -> a
    forall a. LeftClosedPOMonoid a => a -> a -> a
    inverseCompose a
    x a
    forall a. Monoid a => a
    mempty a -> a -> a
    forall a. Semigroup a => a -> a -> a
    <> a
    x) PartialOrdering
    POLE a
    forall a. Monoid a => a
    mempty
      -- It is enough to check the above, because of the following proof:
      -- I will write _\_ for `inverseCompose`, id for mempty, and _._ for (<>).
      -- Assume (*) x^-1 . x <= id, as checked.
      -- Show x^-1 . y <=> x \ y
      --
      -- 1. (>=)
         -- id     <= x . (x \ id)      (galois)
         -- id . y <= x . (x \ id) . y
         -- y      <= x . (x \ id) . y
         -- x \ y  <= (x \ id) . y      (galois)
         -- x^-1 . y >= x \ y           qed
      --
      -- 2. (<=)
         --        y <=        x . (x \ y)   (galois)
         -- x^-1 . y <= x^-1 . x . (x \ y)
         --          <= id       . (x \ y)   (*)
         --          <= x \ y
         -- x^-1 . y <= x \ y                qed