    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Some algebraic structures defined over some other structure
    ------------------------------------------------------------------------

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

    module Algebra.Module.Structures where

    open import Algebra.Bundles
      using (Semiring; Ring; CommutativeSemiring; CommutativeRing)
    open import Algebra.Core using (Op₁; Op₂)
    open import Algebra.Module.Core  using (Opₗ; Opᵣ)
    import Algebra.Definitions as Defs
    open import Algebra.Module.Definitions
      using (module LeftDefs; module RightDefs; module BiDefs
            ; module SimultaneousBiDefs)
    open import Algebra.Structures using (IsCommutativeMonoid; IsAbelianGroup)
    open import Data.Product.Base using (_,_; proj₁; proj₂)
    open import Level using (Level; _⊔_)
    open import Relation.Binary.Core using (Rel)
    open import Relation.Binary.Bundles using (Setoid)
    open import Relation.Binary.Structures using (IsEquivalence)

    private
      variable
        m ℓm r ℓr s ℓs : Level
        M : Set m

    module _ (semiring : Semiring r ℓr) (≈ᴹ : Rel {m} M ℓm) (+ᴹ : Op₂ M) (0ᴹ : M)
      where

      open Semiring semiring renaming (Carrier to R)

      record IsPreleftSemimodule (*ₗ : Opₗ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
        open LeftDefs R ≈ᴹ
        field
          *ₗ-cong : Congruent _≈_ *ₗ
          *ₗ-zeroˡ : LeftZero 0# 0ᴹ *ₗ
          *ₗ-distribʳ : *ₗ DistributesOverʳ _+_ ⟶ +ᴹ
          *ₗ-identityˡ : LeftIdentity 1# *ₗ
          *ₗ-assoc : Associative _*_ *ₗ
          *ₗ-zeroʳ : RightZero 0ᴹ *ₗ
          *ₗ-distribˡ : *ₗ DistributesOverˡ +ᴹ

      record IsLeftSemimodule (*ₗ : Opₗ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
        open LeftDefs R ≈ᴹ
        field
          +ᴹ-isCommutativeMonoid : IsCommutativeMonoid ≈ᴹ +ᴹ 0ᴹ
          isPreleftSemimodule : IsPreleftSemimodule *ₗ

        open IsPreleftSemimodule isPreleftSemimodule public

        open IsCommutativeMonoid +ᴹ-isCommutativeMonoid public
          using () renaming
          ( assoc                to +ᴹ-assoc
          ; comm                 to +ᴹ-comm
          ; identity             to +ᴹ-identity
          ; identityʳ            to +ᴹ-identityʳ
          ; identityˡ            to +ᴹ-identityˡ
          ; isEquivalence        to ≈ᴹ-isEquivalence
          ; isMagma              to +ᴹ-isMagma
          ; isMonoid             to +ᴹ-isMonoid
          ; isPartialEquivalence to ≈ᴹ-isPartialEquivalence
          ; isSemigroup          to +ᴹ-isSemigroup
          ; refl                 to ≈ᴹ-refl
          ; reflexive            to ≈ᴹ-reflexive
          ; setoid               to ≈ᴹ-setoid
          ; sym                  to ≈ᴹ-sym
          ; trans                to ≈ᴹ-trans
          ; ∙-cong               to +ᴹ-cong
          ; ∙-congʳ              to +ᴹ-congʳ
          ; ∙-congˡ              to +ᴹ-congˡ
          )

        *ₗ-congˡ : LeftCongruent *ₗ
        *ₗ-congˡ mm = *ₗ-cong refl mm

        *ₗ-congʳ : RightCongruent _≈_ *ₗ
        *ₗ-congʳ xx = *ₗ-cong xx ≈ᴹ-refl

      record IsPrerightSemimodule (*ᵣ : Opᵣ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
        open RightDefs R ≈ᴹ
        field
          *ᵣ-cong : Congruent _≈_ *ᵣ
          *ᵣ-zeroʳ : RightZero 0# 0ᴹ *ᵣ
          *ᵣ-distribˡ : *ᵣ DistributesOverˡ _+_ ⟶ +ᴹ
          *ᵣ-identityʳ : RightIdentity 1# *ᵣ
          *ᵣ-assoc : Associative _*_ *ᵣ
          *ᵣ-zeroˡ : LeftZero 0ᴹ *ᵣ
          *ᵣ-distribʳ : *ᵣ DistributesOverʳ +ᴹ

      record IsRightSemimodule (*ᵣ : Opᵣ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
        open RightDefs R ≈ᴹ
        field
          +ᴹ-isCommutativeMonoid : IsCommutativeMonoid ≈ᴹ +ᴹ 0ᴹ
          isPrerightSemimodule : IsPrerightSemimodule *ᵣ

        open IsPrerightSemimodule isPrerightSemimodule public

        open IsCommutativeMonoid +ᴹ-isCommutativeMonoid public
          using () renaming
          ( assoc                to +ᴹ-assoc
          ; comm                 to +ᴹ-comm
          ; identity             to +ᴹ-identity
          ; identityʳ            to +ᴹ-identityʳ
          ; identityˡ            to +ᴹ-identityˡ
          ; isEquivalence        to ≈ᴹ-isEquivalence
          ; isMagma              to +ᴹ-isMagma
          ; isMonoid             to +ᴹ-isMonoid
          ; isPartialEquivalence to ≈ᴹ-isPartialEquivalence
          ; isSemigroup          to +ᴹ-isSemigroup
          ; refl                 to ≈ᴹ-refl
          ; reflexive            to ≈ᴹ-reflexive
          ; setoid               to ≈ᴹ-setoid
          ; sym                  to ≈ᴹ-sym
          ; trans                to ≈ᴹ-trans
          ; ∙-cong               to +ᴹ-cong
          ; ∙-congʳ              to +ᴹ-congʳ
          ; ∙-congˡ              to +ᴹ-congˡ
          )

        *ᵣ-congˡ : LeftCongruent _≈_ *ᵣ
        *ᵣ-congˡ xx = *ᵣ-cong ≈ᴹ-refl xx

        *ᵣ-congʳ : RightCongruent *ᵣ
        *ᵣ-congʳ mm = *ᵣ-cong mm refl

    module _ (R-semiring : Semiring r ℓr) (S-semiring : Semiring s ℓs)
             (≈ᴹ : Rel {m} M ℓm) (+ᴹ : Op₂ M) (0ᴹ : M)
      where

      open Semiring R-semiring using () renaming (Carrier to R)
      open Semiring S-semiring using () renaming (Carrier to S)

      record IsBisemimodule (*ₗ : Opₗ R M) (*ᵣ : Opᵣ S M)
                            : Set (r ⊔ s ⊔ m ⊔ ℓr ⊔ ℓs ⊔ ℓm) where
        open BiDefs R S ≈ᴹ
        field
          +ᴹ-isCommutativeMonoid : IsCommutativeMonoid ≈ᴹ +ᴹ 0ᴹ
          isPreleftSemimodule : IsPreleftSemimodule R-semiring ≈ᴹ +ᴹ 0ᴹ *ₗ
          isPrerightSemimodule : IsPrerightSemimodule S-semiring ≈ᴹ +ᴹ 0ᴹ *ᵣ
          *ₗ-*ᵣ-assoc : Associative *ₗ *ᵣ

        isLeftSemimodule : IsLeftSemimodule R-semiring ≈ᴹ +ᴹ 0ᴹ *ₗ
        isLeftSemimodule = record
          { +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid
          ; isPreleftSemimodule = isPreleftSemimodule
          }

        isRightSemimodule : IsRightSemimodule S-semiring ≈ᴹ +ᴹ 0ᴹ *ᵣ
        isRightSemimodule = record
          { +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid
          ; isPrerightSemimodule = isPrerightSemimodule
          }

        open IsLeftSemimodule isLeftSemimodule public
          hiding (+ᴹ-isCommutativeMonoid; isPreleftSemimodule)
        open IsPrerightSemimodule isPrerightSemimodule public
        open IsRightSemimodule isRightSemimodule public
          using (*ᵣ-congˡ; *ᵣ-congʳ)

    module _ (commutativeSemiring : CommutativeSemiring r ℓr)
             (≈ᴹ : Rel {m} M ℓm) (+ᴹ : Op₂ M) (0ᴹ : M)
      where

      open CommutativeSemiring commutativeSemiring renaming (Carrier to R)

      -- An R-semimodule is an R-R-bisemimodule where R is commutative.
      -- We enforce that *ₗ and *ᵣ coincide up to mathematical equality, though it
      -- may be that they do not coincide up to definitional equality.

      open SimultaneousBiDefs R ≈ᴹ

      record IsSemimodule (*ₗ : Opₗ R M) (*ᵣ : Opᵣ R M)
                          : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
        field
          isBisemimodule : IsBisemimodule semiring semiring ≈ᴹ +ᴹ 0ᴹ *ₗ *ᵣ
          *ₗ-*ᵣ-coincident : Coincident *ₗ *ᵣ

        open IsBisemimodule isBisemimodule public

    module _ (ring : Ring r ℓr)
             (≈ᴹ : Rel {m} M ℓm) (+ᴹ : Op₂ M) (0ᴹ : M) (-ᴹ : Op₁ M)
      where

      open Ring ring renaming (Carrier to R)

      record IsLeftModule (*ₗ : Opₗ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
        open Defs ≈ᴹ
        field
          isLeftSemimodule : IsLeftSemimodule semiring ≈ᴹ +ᴹ 0ᴹ *ₗ
          -ᴹ‿cong : Congruent₁ -ᴹ
          -ᴹ‿inverse : Inverse 0ᴹ -ᴹ +ᴹ

        open IsLeftSemimodule isLeftSemimodule public

        +ᴹ-isAbelianGroup : IsAbelianGroup ≈ᴹ +ᴹ 0ᴹ -ᴹ
        +ᴹ-isAbelianGroup = record
          { isGroup = record
            { isMonoid = +ᴹ-isMonoid
            ; inverse = -ᴹ‿inverse
            ; ⁻¹-cong = -ᴹ‿cong
            }
          ; comm = +ᴹ-comm
          }

        open IsAbelianGroup +ᴹ-isAbelianGroup public
          using () renaming
          ( isGroup    to +ᴹ-isGroup
          ; inverseˡ   to -ᴹ‿inverseˡ
          ; inverseʳ   to -ᴹ‿inverseʳ
          ; uniqueˡ-⁻¹ to uniqueˡ‿-ᴹ
          ; uniqueʳ-⁻¹ to uniqueʳ‿-ᴹ
          )
        {-# WARNING_ON_USAGE uniqueˡ‿-ᴹ
        "Warning: uniqueˡ‿-ᴹ was deprecated in v2.3.
        Please use Algebra.Module.Properties.LeftModule.inverseˡ-uniqueᴹ instead."
        #-}
        {-# WARNING_ON_USAGE uniqueʳ‿-ᴹ
        "Warning: uniqueʳ‿-ᴹ was deprecated in v2.3.
        Please use Algebra.Module.Properties.LeftModule.inverseʳ-uniqueᴹ instead."
        #-}

      record IsRightModule (*ᵣ : Opᵣ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
        open Defs ≈ᴹ
        field
          isRightSemimodule : IsRightSemimodule semiring ≈ᴹ +ᴹ 0ᴹ *ᵣ
          -ᴹ‿cong : Congruent₁ -ᴹ
          -ᴹ‿inverse : Inverse 0ᴹ -ᴹ +ᴹ

        open IsRightSemimodule isRightSemimodule public

        +ᴹ-isAbelianGroup : IsAbelianGroup ≈ᴹ +ᴹ 0ᴹ -ᴹ
        +ᴹ-isAbelianGroup = record
          { isGroup = record
            { isMonoid = +ᴹ-isMonoid
            ; inverse = -ᴹ‿inverse
            ; ⁻¹-cong = -ᴹ‿cong
            }
          ; comm = +ᴹ-comm
          }

        open IsAbelianGroup +ᴹ-isAbelianGroup public
          using () renaming
          ( isGroup    to +ᴹ-isGroup
          ; inverseˡ   to -ᴹ‿inverseˡ
          ; inverseʳ   to -ᴹ‿inverseʳ
          ; uniqueˡ-⁻¹ to uniqueˡ‿-ᴹ
          ; uniqueʳ-⁻¹ to uniqueʳ‿-ᴹ
          )
        {-# WARNING_ON_USAGE uniqueˡ‿-ᴹ
        "Warning: uniqueˡ‿-ᴹ was deprecated in v2.3.
        Please use Algebra.Module.Properties.RightModule.inverseˡ-uniqueᴹ instead."
        #-}
        {-# WARNING_ON_USAGE uniqueʳ‿-ᴹ
        "Warning: uniqueʳ‿-ᴹ was deprecated in v2.3.
        Please use Algebra.Module.Properties.RightModule.inverseʳ-uniqueᴹ instead."
        #-}

    module _ (R-ring : Ring r ℓr) (S-ring : Ring s ℓs)
             (≈ᴹ : Rel {m} M ℓm) (+ᴹ : Op₂ M) (0ᴹ : M) (-ᴹ : Op₁ M)
      where

      open Ring R-ring renaming (Carrier to R; semiring to R-semiring)
      open Ring S-ring renaming (Carrier to S; semiring to S-semiring)

      record IsBimodule (*ₗ : Opₗ R M) (*ᵣ : Opᵣ S M)
                        : Set (r ⊔ s ⊔ m ⊔ ℓr ⊔ ℓs ⊔ ℓm) where
        open Defs ≈ᴹ
        field
          isBisemimodule : IsBisemimodule R-semiring S-semiring ≈ᴹ +ᴹ 0ᴹ *ₗ *ᵣ
          -ᴹ‿cong : Congruent₁ -ᴹ
          -ᴹ‿inverse : Inverse 0ᴹ -ᴹ +ᴹ

        open IsBisemimodule isBisemimodule public

        isLeftModule : IsLeftModule R-ring ≈ᴹ +ᴹ 0ᴹ -ᴹ *ₗ
        isLeftModule = record
          { isLeftSemimodule = isLeftSemimodule
          ; -ᴹ‿cong = -ᴹ‿cong
          ; -ᴹ‿inverse = -ᴹ‿inverse
          }

        open IsLeftModule isLeftModule public
          using ( +ᴹ-isAbelianGroup; +ᴹ-isGroup; -ᴹ‿inverseˡ; -ᴹ‿inverseʳ
                ; uniqueˡ‿-ᴹ; uniqueʳ‿-ᴹ)

        isRightModule : IsRightModule S-ring ≈ᴹ +ᴹ 0ᴹ -ᴹ *ᵣ
        isRightModule = record
          { isRightSemimodule = isRightSemimodule
          ; -ᴹ‿cong = -ᴹ‿cong
          ; -ᴹ‿inverse = -ᴹ‿inverse
          }

    module _ (commutativeRing : CommutativeRing r ℓr)
             (≈ᴹ : Rel {m} M ℓm) (+ᴹ : Op₂ M) (0ᴹ : M) (-ᴹ : Op₁ M)
      where

      open CommutativeRing commutativeRing renaming (Carrier to R)

      -- An R-module is an R-R-bimodule where R is commutative.
      -- We enforce that *ₗ and *ᵣ coincide up to mathematical equality, though it
      -- may be that they do not coincide up to definitional equality.

      open SimultaneousBiDefs R ≈ᴹ

      record IsModule (*ₗ : Opₗ R M) (*ᵣ : Opᵣ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
        field
          isBimodule : IsBimodule ring ring ≈ᴹ +ᴹ 0ᴹ -ᴹ *ₗ *ᵣ
          *ₗ-*ᵣ-coincident : Coincident *ₗ *ᵣ

        open IsBimodule isBimodule public

        isSemimodule : IsSemimodule commutativeSemiring ≈ᴹ +ᴹ 0ᴹ *ₗ *ᵣ
        isSemimodule = record { isBisemimodule = isBisemimodule; *ₗ-*ᵣ-coincident = *ₗ-*ᵣ-coincident }