Agda-2.5.3.20180519: A dependently typed functional programming language and proof assistant

Safe HaskellSafe
LanguageHaskell2010

Agda.Utils.POMonoid

Description

Partially ordered monoids.

Synopsis

Documentation

class (PartialOrd a, Semigroup a) => POSemigroup a Source #

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, Monoid a) => POMonoid a Source #

Partially ordered monoid.

Law: composition must be monotone.

  related x POLE x' && related y POLE y' ==>
  related (x <> y) POLE (x' <> y')

class POMonoid a => LeftClosedPOMonoid a where Source #

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)

Minimal complete definition

inverseCompose

Methods

inverseCompose :: a -> a -> a Source #