Safe Haskell | Safe |
---|---|

Language | Haskell2010 |

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

Defined in Agda.Syntax.Common | |

POSemigroup Quantity Source # | |

Defined in Agda.Syntax.Common | |

POSemigroup Modality Source # | |

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

Defined in Agda.Syntax.Common | |

POMonoid Quantity Source # | |

Defined in Agda.Syntax.Common | |

POMonoid Modality 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)

inverseCompose :: a -> a -> a Source #

## Instances

LeftClosedPOMonoid Relevance Source # | |

Defined in Agda.Syntax.Common | |

LeftClosedPOMonoid Quantity Source # | |

Defined in Agda.Syntax.Common | |

LeftClosedPOMonoid Modality Source # | |

Defined in Agda.Syntax.Common |