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

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

    open import Algebra.Bundles        using (CommutativeRing)
    open import Algebra.Module.Bundles using (Module)
    open import Level                  using (Level)

    module Algebra.Module.Properties
      {r ℓr m ℓm : Level}
      {ring      : CommutativeRing r ℓr}
      (mod       : Module ring m ℓm)
      where

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