Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
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')

Instances

Instances details
POSemigroup (UnderAddition Cohesion) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderAddition Modality) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderAddition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderAddition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderComposition Cohesion) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderComposition Modality) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderComposition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

POSemigroup (UnderComposition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

class (PartialOrd a, Semigroup 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')

Instances

Instances details
POMonoid (UnderAddition Cohesion) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderAddition Modality) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderAddition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderAddition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderComposition Cohesion) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderComposition Modality) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderComposition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

POMonoid (UnderComposition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

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)

Methods

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

hasLeftAdjoint :: LeftClosedPOMonoid a => a -> Bool Source #

hasLeftAdjoint x checks whether x^-1 := x inverseCompose mempty is such that x inverseCompose y == x^-1 <> y for any y.