    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Definitions of algebraic structures like monoids and rings
    -- (packed in records together with sets, operations, etc.)
    ------------------------------------------------------------------------

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

    module Algebra where

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