    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Instances of algebraic structures where the carrier is ⊤. In
    -- mathematics, this is usually called 0 (1 in the case of Monoid, Group).
    --
    -- From monoids up, these are are zero-objects – i.e, both the initial
    -- and the terminal object in the relevant category.
    --
    -- For structures without an identity element, the terminal algebra is
    -- *not*  initial, because there is an instance of such a structure
    -- with an empty Carrier. Accordingly, such definitions are now deprecated
    -- in favour of those defined in `Algebra.Construct.Terminal`.
    ------------------------------------------------------------------------

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

    open import Level using (Level)

    module Algebra.Construct.Zero {c ℓ : Level} where

    open import Algebra.Bundles.Raw using (RawMagma)
    open import Algebra.Bundles using (Magma; Semigroup; Band)

    ------------------------------------------------------------------------
    -- Re-export those algebras which are both initial and terminal

    open import Algebra.Construct.Terminal public
      hiding (rawMagma; magma; semigroup; band)

    ------------------------------------------------------------------------
    -- DEPRECATED
    ------------------------------------------------------------------------
    -- Please use the new definitions re-exported from
    -- `Algebra.Construct.Terminal` as continuing support for the below is
    -- not guaranteed.

    -- Version 2.0

    rawMagma : RawMagma c ℓ
    rawMagma = Algebra.Construct.Terminal.rawMagma

    {-# WARNING_ON_USAGE rawMagma
    "Warning: rawMagma was deprecated in v2.0.
    Please use Algebra.Construct.Terminal.rawMagma instead."
    #-}

    magma : Magma c ℓ
    magma = Algebra.Construct.Terminal.magma
    {-# WARNING_ON_USAGE magma
    "Warning: magma was deprecated in v2.0.
    Please use Algebra.Construct.Terminal.magma instead."
    #-}

    semigroup : Semigroup c ℓ
    semigroup = Algebra.Construct.Terminal.semigroup
    {-# WARNING_ON_USAGE semigroup
    "Warning: semigroup was deprecated in v2.0.
    Please use Algebra.Construct.Terminal.semigroup instead."
    #-}

    band : Band c ℓ
    band = Algebra.Construct.Terminal.band
    {-# WARNING_ON_USAGE semigroup
    "Warning: semigroup was deprecated in v2.0.
    Please use Algebra.Construct.Terminal.semigroup instead."
    #-}