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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Utils.POMonoid

Description

Partially ordered monoids.

Synopsis

- class (PartialOrd a, Semigroup a) => POSemigroup a
- class (PartialOrd a, Semigroup a, Monoid a) => POMonoid a
- class POMonoid a => LeftClosedPOMonoid a where
  - inverseCompose :: a -> a -> a
- hasLeftAdjoint :: LeftClosedPOMonoid a => a -> Bool

# 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 #

#### Instances

Instances details

LeftClosedPOMonoid (UnderComposition Cohesion) Source # |
Instance details Defined in Agda.Syntax.Common Methods inverseCompose :: UnderComposition Cohesion -> UnderComposition Cohesion -> UnderComposition Cohesion Source #
LeftClosedPOMonoid (UnderComposition Modality) Source # |
Instance details Defined in Agda.Syntax.Common Methods inverseCompose :: UnderComposition Modality -> UnderComposition Modality -> UnderComposition Modality Source #
LeftClosedPOMonoid (UnderComposition Quantity) Source # |
Instance details Defined in Agda.Syntax.Common Methods inverseCompose :: UnderComposition Quantity -> UnderComposition Quantity -> UnderComposition Quantity Source #
LeftClosedPOMonoid (UnderComposition Relevance) Source # |
Instance details Defined in Agda.Syntax.Common Methods inverseCompose :: UnderComposition Relevance -> UnderComposition Relevance -> UnderComposition Relevance 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`.