1{-# LANGUAGE CPP #-} 2-- | Partially ordered monoids. 3 4module Agda.Utils.POMonoid where 5 6#if __GLASGOW_HASKELL__ < 804 7import Data.Semigroup 8#endif 9 10import Agda.Utils.PartialOrd 11 12-- | Partially ordered semigroup. 13-- 14-- Law: composition must be monotone. 15-- 16-- @ 17-- related x POLE x' && related y POLE y' ==> 18-- related (x <> y) POLE (x' <> y') 19-- @ 20 21class (PartialOrd a, Semigroup a) => POSemigroup a where 22 23-- | Partially ordered monoid. 24-- 25-- Law: composition must be monotone. 26-- 27-- @ 28-- related x POLE x' && related y POLE y' ==> 29-- related (x <> y) POLE (x' <> y') 30-- @ 31 32class (PartialOrd a, Semigroup a, Monoid a) => POMonoid a where 33 34-- | Completing POMonoids with inverses to form a Galois connection. 35-- 36-- Law: composition and inverse composition form a Galois connection. 37-- 38-- @ 39-- related (inverseCompose p x) POLE y <==> related x POLE (p <> y) 40-- @ 41 42class POMonoid a => LeftClosedPOMonoid a where 43 inverseCompose :: a -> a -> a 44 45 46-- | @hasLeftAdjoint x@ checks whether 47-- @x^-1 := x `inverseCompose` mempty@ is such that 48-- @x `inverseCompose` y == x^-1 <> y@ for any @y@. 49hasLeftAdjoint :: LeftClosedPOMonoid a => a -> Bool 50hasLeftAdjoint x = related (inverseCompose x mempty <> x) POLE mempty 51 -- It is enough to check the above, because of the following proof: 52 -- I will write _\_ for `inverseCompose`, id for mempty, and _._ for (<>). 53 -- Assume (*) x^-1 . x <= id, as checked. 54 -- Show x^-1 . y <=> x \ y 55 -- 56 -- 1. (>=) 57 -- id <= x . (x \ id) (galois) 58 -- id . y <= x . (x \ id) . y 59 -- y <= x . (x \ id) . y 60 -- x \ y <= (x \ id) . y (galois) 61 -- x^-1 . y >= x \ y qed 62 -- 63 -- 2. (<=) 64 -- y <= x . (x \ y) (galois) 65 -- x^-1 . y <= x^-1 . x . (x \ y) 66 -- <= id . (x \ y) (*) 67 -- <= x \ y 68 -- x^-1 . y <= x \ y qed 69