    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Definitions of algebraic structure module
    -- packed in records together with sets, operations, etc.
    ------------------------------------------------------------------------

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

    module Algebra.Module where

    open import Algebra.Module.Core public
    open import Algebra.Module.Structures public
    open import Algebra.Module.Structures.Biased public
    open import Algebra.Module.Bundles public
    open import Algebra.Module.Definitions public