------------------------------------------------------------------------
-- The Agda standard library
--
-- Definitions of ordered algebraic structures like promonoids and
-- posemigroups (packed in records together with sets, orders,
-- operations, etc.)
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Algebra.Ordered where

open import Algebra.Ordered.Structures public
open import Algebra.Ordered.Bundles public