Semigroup package:Agda

module Agda.Utils.Semigroup
Agda
Some semigroup instances used in several places
class Semigroup a
Agda Agda.Utils.Semigroup
The class of semigroups (types with an associative binary operation). Instances should satisfy the following:
  • Associativity x <> (y <> z) = (x <> y) <> z
You can alternatively define sconcat instead of (<>), in which case the laws are:
class (PartialOrd a, Semigroup a) => POSemigroup a
Agda Agda.Utils.POMonoid
Partially ordered semigroup. Law: composition must be monotone. 
related x POLE x' && related y POLE y' ==>
related (x <> y) POLE (x' <> y')