    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- The unique morphism from the initial object,
    -- for each of the relevant categories. Since
    -- `Semigroup` and `Band` are simply `Magma`s
    -- satisfying additional properties, it suffices to
    -- define the morphism on the underlying `RawMagma`.
    ------------------------------------------------------------------------

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

    open import Level using (Level)

    module Algebra.Morphism.Construct.Initial {c ℓ : Level} where

    open import Algebra.Bundles.Raw using (RawMagma)
    open import Algebra.Morphism.Structures
      using (IsMagmaHomomorphism; IsMagmaMonomorphism)
    open import Function.Definitions using (Injective)
    import Relation.Binary.Morphism.Definitions as Rel
    open import Relation.Binary.Core using (Rel)

    open import Algebra.Construct.Initial {c} {ℓ}

    private
      variable
        a m ℓm : Level
        A : Set a
        ≈ : Rel A ℓm

    ------------------------------------------------------------------------
    -- The unique morphism

    zero : ℤero.Carrier → A
    zero ()

    ------------------------------------------------------------------------
    -- Basic properties

    cong : (≈ : Rel A ℓm) → Rel.Homomorphic₂ ℤero.Carrier A ℤero._≈_ ≈ zero
    cong _ {x = ()}

    injective : (≈ : Rel A ℓm) → Injective ℤero._≈_ ≈ zero
    injective _ {x = ()}

    ------------------------------------------------------------------------
    -- Morphism structures

    isMagmaHomomorphism : (M : RawMagma m ℓm) →
                          IsMagmaHomomorphism rawMagma M zero
    isMagmaHomomorphism M = record
      { isRelHomomorphism = record { cong = cong (RawMagma._≈_ M) }
      ; homo = λ()
      }

    isMagmaMonomorphism : (M : RawMagma m ℓm) →
                          IsMagmaMonomorphism rawMagma M zero
    isMagmaMonomorphism M = record
      { isMagmaHomomorphism = isMagmaHomomorphism M
      ; injective = injective (RawMagma._≈_ M)
      }