Monoid package:Agda

module Agda.Utils.Monoid
Agda
More monoids.
module Agda.Utils.POMonoid
Agda
Partially ordered monoids.
class POMonoid a => LeftClosedPOMonoid a
Agda Agda.Utils.POMonoid
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 (PartialOrd a, Semigroup a, Monoid a) => POMonoid a
Agda Agda.Utils.POMonoid
Partially ordered monoid. Law: composition must be monotone. 
related x POLE x' && related y POLE y' ==>
related (x <> y) POLE (x' <> y')