Agda-2.6.1.3: 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 Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

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, 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 Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

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

Instances details
LeftClosedPOMonoid Cohesion Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

inverseCompose :: Cohesion -> Cohesion -> Cohesion Source #

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 #

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.