    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Consequences of a monomorphism between bisemimodules
    ------------------------------------------------------------------------

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

    open import Algebra.Module.Bundles.Raw using (RawBisemimodule)
    open import Algebra.Module.Morphism.Structures using (IsBisemimoduleMonomorphism)

    module Algebra.Module.Morphism.BisemimoduleMonomorphism
      {r s a b ℓ₁ ℓ₂} {R : Set r} {S : Set s} {M : RawBisemimodule R S a ℓ₁} {N : RawBisemimodule R S b ℓ₂} {⟦_⟧}
      (isBisemimoduleMonomorphism : IsBisemimoduleMonomorphism M N ⟦_⟧)
      where

    open IsBisemimoduleMonomorphism isBisemimoduleMonomorphism
    private
      module M = RawBisemimodule M
      module N = RawBisemimodule N

    open import Algebra.Bundles using (Semiring)
    open import Algebra.Core using (Op₂)
    import Algebra.Module.Definitions.Bi as BiDefs using (Associative)
    import Algebra.Module.Definitions.Left as LeftDefs using (LeftCongruent)
    import Algebra.Module.Definitions.Right as RightDefs using (RightCongruent)
    open import Algebra.Module.Structures using (IsBisemimodule)
    open import Algebra.Structures using (IsMagma; IsSemiring)
    open import Function.Base using (flip; _$_)
    open import Relation.Binary.Core using (Rel)
    import Relation.Binary.Reasoning.Setoid as SetoidReasoning

    ------------------------------------------------------------------------
    -- Re-exports

    open import Algebra.Morphism.MonoidMonomorphism
      +ᴹ-isMonoidMonomorphism public
        using ()
        renaming
          ( cong to +ᴹ-cong
          ; assoc to +ᴹ-assoc
          ; comm to +ᴹ-comm
          ; identityˡ to +ᴹ-identityˡ
          ; identityʳ to +ᴹ-identityʳ
          ; identity to +ᴹ-identity
          ; isMagma to +ᴹ-isMagma
          ; isSemigroup to +ᴹ-isSemigroup
          ; isMonoid to +ᴹ-isMonoid
          ; isCommutativeMonoid to +ᴹ-isCommutativeMonoid
          )

    open import Algebra.Module.Morphism.LeftSemimoduleMonomorphism
      isLeftSemimoduleMonomorphism public
      using
        ( *ₗ-cong
        ; *ₗ-zeroˡ
        ; *ₗ-distribʳ
        ; *ₗ-identityˡ
        ; *ₗ-assoc
        ; *ₗ-zeroʳ
        ; *ₗ-distribˡ
        ; isLeftSemimodule
        )

    open import Algebra.Module.Morphism.RightSemimoduleMonomorphism
      isRightSemimoduleMonomorphism public
      using
        ( *ᵣ-cong
        ; *ᵣ-zeroʳ
        ; *ᵣ-distribˡ
        ; *ᵣ-identityʳ
        ; *ᵣ-assoc
        ; *ᵣ-zeroˡ
        ; *ᵣ-distribʳ
        ; isRightSemimodule
        )

    ------------------------------------------------------------------------
    -- Properties

    module _ (+ᴹ-isMagma : IsMagma N._≈ᴹ_ N._+ᴹ_) where

      open IsMagma +ᴹ-isMagma
        using (setoid)
        renaming (∙-cong to +ᴹ-cong)
      open SetoidReasoning setoid

      private
        module MDefs = BiDefs R S M._≈ᴹ_
        module NDefs = BiDefs R S N._≈ᴹ_
        module LDefs = LeftDefs R N._≈ᴹ_
        module RDefs = RightDefs S N._≈ᴹ_

      *ₗ-*ᵣ-assoc
        : LDefs.LeftCongruent N._*ₗ_ → RDefs.RightCongruent N._*ᵣ_
        → NDefs.Associative N._*ₗ_ N._*ᵣ_
        → MDefs.Associative M._*ₗ_ M._*ᵣ_
      *ₗ-*ᵣ-assoc *ₗ-congˡ *ᵣ-congʳ *ₗ-*ᵣ-assoc x m y = injective $ begin
        ⟦ (x M.*ₗ m) M.*ᵣ y ⟧ ≈⟨ *ᵣ-homo y (x M.*ₗ m) ⟩
        ⟦ x M.*ₗ m ⟧ N.*ᵣ y   ≈⟨ *ᵣ-congʳ (*ₗ-homo x m) ⟩
        (x N.*ₗ ⟦ m ⟧) N.*ᵣ y ≈⟨ *ₗ-*ᵣ-assoc x ⟦ m ⟧ y ⟩
        x N.*ₗ (⟦ m ⟧ N.*ᵣ y) ≈˘⟨ *ₗ-congˡ (*ᵣ-homo y m) ⟩
        x N.*ₗ ⟦ m M.*ᵣ y ⟧   ≈˘⟨ *ₗ-homo x (m M.*ᵣ y) ⟩
        ⟦ x M.*ₗ (m M.*ᵣ y) ⟧ ∎

    ------------------------------------------------------------------------
    -- Structures

    module _
      {ℓr} {_≈r_ : Rel R ℓr} {_+r_ _*r_ 0r 1r}
      {ℓs} {_≈s_ : Rel S ℓs} {_+s_ _*s_ 0s 1s}
      (R-isSemiring : IsSemiring _≈r_ _+r_ _*r_ 0r 1r)
      (S-isSemiring : IsSemiring _≈s_ _+s_ _*s_ 0s 1s)
      where

      private
        R-semiring : Semiring _ _
        R-semiring = record { isSemiring = R-isSemiring }

        S-semiring : Semiring _ _
        S-semiring = record { isSemiring = S-isSemiring }

      isBisemimodule
        : IsBisemimodule R-semiring S-semiring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N._*ₗ_ N._*ᵣ_
        → IsBisemimodule R-semiring S-semiring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M._*ₗ_ M._*ᵣ_
      isBisemimodule isBisemimodule = record
        { +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid NN.+ᴹ-isCommutativeMonoid
        ; isPreleftSemimodule = record
          { *ₗ-cong = *ₗ-cong NN.+ᴹ-isMagma NN.*ₗ-cong
          ; *ₗ-zeroˡ = *ₗ-zeroˡ NN.+ᴹ-isMagma NN.*ₗ-zeroˡ
          ; *ₗ-distribʳ = *ₗ-distribʳ NN.+ᴹ-isMagma NN.*ₗ-distribʳ
          ; *ₗ-identityˡ = *ₗ-identityˡ NN.+ᴹ-isMagma NN.*ₗ-identityˡ
          ; *ₗ-assoc = *ₗ-assoc NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-assoc
          ; *ₗ-zeroʳ = *ₗ-zeroʳ NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-zeroʳ
          ; *ₗ-distribˡ = *ₗ-distribˡ NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-distribˡ
          }
        ; isPrerightSemimodule = record
          { *ᵣ-cong = *ᵣ-cong NN.+ᴹ-isMagma NN.*ᵣ-cong
          ; *ᵣ-zeroʳ = *ᵣ-zeroʳ NN.+ᴹ-isMagma NN.*ᵣ-zeroʳ
          ; *ᵣ-distribˡ = *ᵣ-distribˡ NN.+ᴹ-isMagma NN.*ᵣ-distribˡ
          ; *ᵣ-identityʳ = *ᵣ-identityʳ NN.+ᴹ-isMagma NN.*ᵣ-identityʳ
          ; *ᵣ-assoc = *ᵣ-assoc NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-assoc
          ; *ᵣ-zeroˡ = *ᵣ-zeroˡ NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-zeroˡ
          ; *ᵣ-distribʳ = *ᵣ-distribʳ NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-distribʳ
          }
        ; *ₗ-*ᵣ-assoc = *ₗ-*ᵣ-assoc NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ᵣ-congʳ NN.*ₗ-*ᵣ-assoc
        }
        where
          module NN = IsBisemimodule isBisemimodule