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

Safe Haskell | Safe
Language | Haskell2010

Agda.Utils.POMonoid

Description

Partially ordered monoids.

Synopsis

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

# 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

POSemigroup Relevance Source # |
Instance details Defined in Agda.Syntax.Common
POSemigroup Quantity Source # |
Instance details Defined in Agda.Syntax.Common
POSemigroup Modality Source # |
Instance details Defined in Agda.Syntax.Common

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')

Instances

POMonoid Relevance Source # |
Instance details Defined in Agda.Syntax.Common
POMonoid Quantity Source # |
Instance details Defined in Agda.Syntax.Common
POMonoid Modality 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

LeftClosedPOMonoid Relevance Source # |
Instance details Defined in Agda.Syntax.Common Methods inverseCompose :: Relevance -> Relevance -> Relevance Source #
LeftClosedPOMonoid Quantity Source # |
Instance details Defined in Agda.Syntax.Common Methods inverseCompose :: Quantity -> Quantity -> Quantity Source #
LeftClosedPOMonoid Modality Source # |
Instance details Defined in Agda.Syntax.Common Methods inverseCompose :: Modality -> Modality -> Modality Source #