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

-- The contents of this module should be accessed via `Algebra.Ordered`.

{-# OPTIONS --without-K --safe #-}

module Algebra.Ordered.Bundles where

open import Algebra.Core
open import Algebra.Bundles
open import Algebra.Ordered.Structures
open import Level using (suc; _⊔_)
open import Relation.Binary using (Rel)
open import Relation.Binary.Bundles using (Preorder; Poset)

------------------------------------------------------------------------
-- Bundles of preordered structures

-- Preordered magmas (promagmas)

record Promagma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix  4 _≈_ _≤_
  infixl 7 _∙_
  field
    Carrier    : Set c
    _≈_        : Rel Carrier ℓ₁  -- The underlying equality.
    _≤_        : Rel Carrier ℓ₂  -- The preorder.
    _∙_        : Op₂ Carrier     -- Multiplication.
    isPromagma : IsPromagma _≈_ _≤_ _∙_

  open IsPromagma isPromagma public

  preorder : Preorder c ℓ₁ ℓ₂
  preorder = record { isPreorder = isPreorder }

  magma : Magma c ℓ₁
  magma = record { isMagma = isMagma }

-- Preordered semigroups (prosemigroups)

record Prosemigroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix  4 _≈_ _≤_
  infixl 7 _∙_
  field
    Carrier        : Set c
    _≈_            : Rel Carrier ℓ₁  -- The underlying equality.
    _≤_            : Rel Carrier ℓ₂  -- The preorder.
    _∙_            : Op₂ Carrier     -- Multiplication.
    isProsemigroup : IsProsemigroup _≈_ _≤_ _∙_

  open IsProsemigroup isProsemigroup public

  promagma : Promagma c ℓ₁ ℓ₂
  promagma = record { isPromagma = isPromagma }

  open Promagma promagma public using (preorder; magma)

  semigroup : Semigroup c ℓ₁
  semigroup = record { isSemigroup = isSemigroup }

-- Preordered monoids (promonoids)

record Promonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix  4 _≈_ _≤_
  infixl 7 _∙_
  field
    Carrier     : Set c
    _≈_         : Rel Carrier ℓ₁  -- The underlying equality.
    _≤_         : Rel Carrier ℓ₂  -- The preorder.
    _∙_         : Op₂ Carrier     -- The monoid multiplication.
    ε           : Carrier         -- The monoid unit.
    isPromonoid : IsPromonoid _≈_ _≤_ _∙_ ε

  open IsPromonoid isPromonoid public

  prosemigroup : Prosemigroup c ℓ₁ ℓ₂
  prosemigroup = record { isProsemigroup = isProsemigroup }

  open Prosemigroup prosemigroup public
    using (preorder; magma; promagma; semigroup)

  monoid : Monoid c ℓ₁
  monoid = record { isMonoid = isMonoid }

-- Preordered commutative monoids (commutative promonoids)

record CommutativePromonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix  4 _≈_ _≤_
  infixl 7 _∙_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ₁  -- The underlying equality.
    _≤_     : Rel Carrier ℓ₂  -- The preorder.
    _∙_     : Op₂ Carrier     -- The monoid multiplication.
    ε       : Carrier         -- The monoid unit.
    isCommutativePromonoid : IsCommutativePromonoid _≈_ _≤_ _∙_ ε

  open IsCommutativePromonoid isCommutativePromonoid public

  promonoid : Promonoid c ℓ₁ ℓ₂
  promonoid = record { isPromonoid = isPromonoid }

  open Promonoid promonoid public
    using (preorder; magma; promagma; semigroup; prosemigroup; monoid)

  commutativeMonoid : CommutativeMonoid c ℓ₁
  commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }

  open CommutativeMonoid commutativeMonoid public using (commutativeSemigroup)

-- Preordered semirings (prosemirings)

record Prosemiring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix  4 _≈_ _≤_
  infixl 7 _*_
  infixl 6 _+_
  field
    Carrier       : Set c
    _≈_           : Rel Carrier ℓ₁
    _≤_           : Rel Carrier ℓ₂
    _+_           : Op₂ Carrier
    _*_           : Op₂ Carrier
    0#            : Carrier
    1#            : Carrier
    isProsemiring : IsProsemiring _≈_ _≤_ _+_ _*_ 0# 1#

  open IsProsemiring isProsemiring public

  +-commutativePromonoid : CommutativePromonoid c ℓ₁ ℓ₂
  +-commutativePromonoid = record
    { isCommutativePromonoid = +-isCommutativePromonoid }

  open CommutativePromonoid +-commutativePromonoid public
    using (preorder)
    renaming
    ( magma                to +-magma
    ; promagma             to +-promagma
    ; semigroup            to +-semigroup
    ; prosemigroup         to +-prosemigroup
    ; monoid               to +-monoid
    ; promonoid            to +-promonoid
    ; commutativeSemigroup to +-commutativeSemigroup
    ; commutativeMonoid    to +-commutativeMonoid
    )

  *-promonoid : Promonoid c ℓ₁ ℓ₂
  *-promonoid = record { isPromonoid = *-isPromonoid }

  open Promonoid *-promonoid public
    using ()
    renaming
    ( magma        to *-magma
    ; promagma     to *-promagma
    ; semigroup    to *-semigroup
    ; prosemigroup to *-prosemigroup
    ; monoid       to *-monoid
    )

  semiring : Semiring c ℓ₁
  semiring = record { isSemiring = isSemiring }

------------------------------------------------------------------------
-- Bundles of partially ordered structures

-- Partially ordered magmas (pomagmas)

record Pomagma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix  4 _≈_ _≤_
  infixl 7 _∙_
  field
    Carrier   : Set c
    _≈_       : Rel Carrier ℓ₁  -- The underlying equality.
    _≤_       : Rel Carrier ℓ₂  -- The partial order.
    _∙_       : Op₂ Carrier     -- Multiplication.
    isPomagma : IsPomagma _≈_ _≤_ _∙_

  open IsPomagma isPomagma public

  poset : Poset c ℓ₁ ℓ₂
  poset = record { isPartialOrder = isPartialOrder }

  promagma : Promagma c ℓ₁ ℓ₂
  promagma = record { isPromagma = isPromagma }

  open Promagma promagma public using (preorder; magma)

-- Partially ordered semigroups (posemigroups)

record Posemigroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix  4 _≈_ _≤_
  infixl 7 _∙_
  field
    Carrier       : Set c
    _≈_           : Rel Carrier ℓ₁  -- The underlying equality.
    _≤_           : Rel Carrier ℓ₂  -- The partial order.
    _∙_           : Op₂ Carrier     -- Multiplication.
    isPosemigroup : IsPosemigroup _≈_ _≤_ _∙_

  open IsPosemigroup isPosemigroup public

  pomagma : Pomagma c ℓ₁ ℓ₂
  pomagma = record { isPomagma = isPomagma }

  open Pomagma pomagma public using (preorder; poset; magma; promagma)

  prosemigroup : Prosemigroup c ℓ₁ ℓ₂
  prosemigroup = record { isProsemigroup = isProsemigroup }

  open Prosemigroup prosemigroup public using (semigroup)

-- Partially ordered monoids (pomonoids)

record Pomonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix  4 _≈_ _≤_
  infixl 7 _∙_
  field
    Carrier    : Set c
    _≈_        : Rel Carrier ℓ₁  -- The underlying equality.
    _≤_        : Rel Carrier ℓ₂  -- The partial order.
    _∙_        : Op₂ Carrier     -- The monoid multiplication.
    ε          : Carrier         -- The monoid unit.
    isPomonoid : IsPomonoid _≈_ _≤_ _∙_ ε

  open IsPomonoid isPomonoid public

  posemigroup : Posemigroup c ℓ₁ ℓ₂
  posemigroup = record { isPosemigroup = isPosemigroup }

  open Posemigroup posemigroup public using
    ( preorder
    ; poset
    ; magma
    ; promagma
    ; pomagma
    ; semigroup
    ; prosemigroup
    )

  promonoid : Promonoid c ℓ₁ ℓ₂
  promonoid = record { isPromonoid = isPromonoid }

  open Promonoid promonoid public using (monoid)

-- Partially ordered commutative monoids (commutative pomonoids)

record CommutativePomonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix  4 _≈_ _≤_
  infixl 7 _∙_
  field
    Carrier               : Set c
    _≈_                   : Rel Carrier ℓ₁  -- The underlying equality.
    _≤_                   : Rel Carrier ℓ₂  -- The partial order.
    _∙_                   : Op₂ Carrier     -- The monoid multiplication.
    ε                     : Carrier         -- The monoid unit.
    isCommutativePomonoid : IsCommutativePomonoid _≈_ _≤_ _∙_ ε

  open IsCommutativePomonoid isCommutativePomonoid public

  pomonoid : Pomonoid c ℓ₁ ℓ₂
  pomonoid = record { isPomonoid = isPomonoid }

  open Pomonoid pomonoid public using
    ( preorder
    ; poset
    ; magma
    ; promagma
    ; pomagma
    ; semigroup
    ; prosemigroup
    ; posemigroup
    ; monoid
    ; promonoid
    )

  commutativePromonoid : CommutativePromonoid c ℓ₁ ℓ₂
  commutativePromonoid =
    record { isCommutativePromonoid = isCommutativePromonoid }

  open CommutativePromonoid commutativePromonoid public
    using (commutativeSemigroup; commutativeMonoid)

-- Partially ordered semirings (posemirings)

record Posemiring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix  4 _≈_ _≤_
  infixl 7 _*_
  infixl 6 _+_
  field
    Carrier      : Set c
    _≈_          : Rel Carrier ℓ₁
    _≤_          : Rel Carrier ℓ₂
    _+_          : Op₂ Carrier
    _*_          : Op₂ Carrier
    0#           : Carrier
    1#           : Carrier
    isPosemiring : IsPosemiring _≈_ _≤_ _+_ _*_ 0# 1#

  open IsPosemiring isPosemiring public

  +-commutativePomonoid : CommutativePomonoid c ℓ₁ ℓ₂
  +-commutativePomonoid = record
    { isCommutativePomonoid = +-isCommutativePomonoid }

  open CommutativePomonoid +-commutativePomonoid public
    using (preorder)
    renaming
    ( magma                to +-magma
    ; promagma             to +-promagma
    ; pomagma              to +-pomagma
    ; semigroup            to +-semigroup
    ; prosemigroup         to +-prosemigroup
    ; posemigroup          to +-posemigroup
    ; monoid               to +-monoid
    ; promonoid            to +-promonoid
    ; pomonoid             to +-pomonoid
    ; commutativeSemigroup to +-commutativeSemigroup
    ; commutativeMonoid    to +-commutativeMonoid
    ; commutativePromonoid to +-commutativePromonoid
    )

  *-pomonoid : Pomonoid c ℓ₁ ℓ₂
  *-pomonoid = record { isPomonoid = *-isPomonoid }

  open Pomonoid *-pomonoid public
    using ()
    renaming
    ( magma        to *-magma
    ; promagma     to *-promagma
    ; pomagma      to *-pomagma
    ; semigroup    to *-semigroup
    ; prosemigroup to *-prosemigroup
    ; posemigroup  to *-posemigroup
    ; monoid       to *-monoid
    ; promonoid    to *-promonoid
    )

  prosemiring : Prosemiring c ℓ₁ ℓ₂
  prosemiring = record { isProsemiring = isProsemiring }

  open Prosemiring prosemiring public using (semiring)