ModuleAgda-2.7.0.1Haskell2010

Agda.Utils.POMonoid

Partially ordered monoids.

classclass (PartialOrd a, Semigroup a) => POSemigroup a

Partially ordered semigroup.

Law: composition must be monotone.

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

Instances8POSemigroup, …

POSemigroup (UnderAddition Cohesion)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
POSemigroup (UnderAddition Modality)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
POSemigroup (UnderAddition Quantity)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
POSemigroup (UnderAddition Relevance)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
POSemigroup (UnderComposition Cohesion)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
POSemigroup (UnderComposition Modality)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
POSemigroup (UnderComposition Quantity)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
POSemigroup (UnderComposition Relevance)Defined in Agda-2.7.0.1 · Agda.Syntax.Common

classclass (PartialOrd a, Semigroup a, Monoid a) => POMonoid a

Partially ordered monoid.

Law: composition must be monotone.

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

Instances8POMonoid, …

POMonoid (UnderAddition Cohesion)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
POMonoid (UnderAddition Modality)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
POMonoid (UnderAddition Quantity)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
POMonoid (UnderAddition Relevance)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
POMonoid (UnderComposition Cohesion)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
POMonoid (UnderComposition Modality)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
POMonoid (UnderComposition Quantity)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
POMonoid (UnderComposition Relevance)Defined in Agda-2.7.0.1 · Agda.Syntax.Common

classclass POMonoid a => LeftClosedPOMonoid a where

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)

Instances4LeftClosedPOMonoid

LeftClosedPOMonoid (UnderComposition Cohesion)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
LeftClosedPOMonoid (UnderComposition Modality)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
LeftClosedPOMonoid (UnderComposition Quantity)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
LeftClosedPOMonoid (UnderComposition Relevance)Defined in Agda-2.7.0.1 · Agda.Syntax.Common

valuehasLeftAdjoint :: LeftClosedPOMonoid a => a -> Bool

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