    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Properties of bimodules.
    ------------------------------------------------------------------------

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

    open import Algebra.Bundles        using (Ring)
    open import Algebra.Module.Bundles using (Bimodule)
    open import Level                  using (Level)

    module Algebra.Module.Properties.Bimodule
      {r ℓr s ℓs m ℓm : Level}
      {ringR : Ring r ℓr} {ringS : Ring s ℓs}
      (mod   : Bimodule ringR ringS m ℓm)
      where

    open Bimodule mod
    open import Algebra.Module.Properties.LeftModule leftModule public
      using (inverseˡ-uniqueᴹ; inverseʳ-uniqueᴹ; -ᴹ-involutive)