------------------------------------------------------------------------
-- 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