content: {-# 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 x = related (inverseCompose x mempty <> x) POLE 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
  