Safe Haskell | None |
---|---|
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
POSemigroup (UnderAddition Cohesion) Source # | |
Defined in Agda.Syntax.Common | |
POSemigroup (UnderAddition Modality) Source # | |
Defined in Agda.Syntax.Common | |
POSemigroup (UnderAddition Quantity) Source # | |
Defined in Agda.Syntax.Common | |
POSemigroup (UnderAddition Relevance) Source # | |
Defined in Agda.Syntax.Common | |
POSemigroup (UnderComposition Cohesion) Source # | |
Defined in Agda.Syntax.Common | |
POSemigroup (UnderComposition Modality) Source # | |
Defined in Agda.Syntax.Common | |
POSemigroup (UnderComposition Quantity) Source # | |
Defined in Agda.Syntax.Common | |
POSemigroup (UnderComposition Relevance) Source # | |
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
POMonoid (UnderAddition Cohesion) Source # | |
Defined in Agda.Syntax.Common | |
POMonoid (UnderAddition Modality) Source # | |
Defined in Agda.Syntax.Common | |
POMonoid (UnderAddition Quantity) Source # | |
Defined in Agda.Syntax.Common | |
POMonoid (UnderAddition Relevance) Source # | |
Defined in Agda.Syntax.Common | |
POMonoid (UnderComposition Cohesion) Source # | |
Defined in Agda.Syntax.Common | |
POMonoid (UnderComposition Modality) Source # | |
Defined in Agda.Syntax.Common | |
POMonoid (UnderComposition Quantity) Source # | |
Defined in Agda.Syntax.Common | |
POMonoid (UnderComposition Relevance) Source # | |
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 (UnderComposition Cohesion) Source # | |
Defined in Agda.Syntax.Common Methods inverseCompose :: UnderComposition Cohesion -> UnderComposition Cohesion -> UnderComposition Cohesion Source # | |
LeftClosedPOMonoid (UnderComposition Modality) Source # | |
Defined in Agda.Syntax.Common Methods inverseCompose :: UnderComposition Modality -> UnderComposition Modality -> UnderComposition Modality Source # | |
LeftClosedPOMonoid (UnderComposition Quantity) Source # | |
Defined in Agda.Syntax.Common Methods inverseCompose :: UnderComposition Quantity -> UnderComposition Quantity -> UnderComposition Quantity Source # | |
LeftClosedPOMonoid (UnderComposition Relevance) Source # | |
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
is such that
inverseCompose
memptyx
for any inverseCompose
y == x^-1 <> yy
.