| 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
Documentation
class (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')
Instances
| POSemigroup Relevance # | |
Defined in Agda.Syntax.Common | |
| POSemigroup Quantity # | |
Defined in Agda.Syntax.Common | |
| POSemigroup Modality # | |
Defined in Agda.Syntax.Common | |
class (PartialOrd 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')
Instances
| POMonoid Relevance # | |
Defined in Agda.Syntax.Common | |
| POMonoid Quantity # | |
Defined in Agda.Syntax.Common | |
| POMonoid Modality # | |
Defined in Agda.Syntax.Common | |
class 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)
Minimal complete definition
Methods
inverseCompose :: a -> a -> a #
Instances
| LeftClosedPOMonoid Relevance # | |
Defined in Agda.Syntax.Common Methods inverseCompose :: Relevance -> Relevance -> Relevance # | |