    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- The projection morphisms for algebraic structures arising from the
    -- direct product construction
    ------------------------------------------------------------------------

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

    module Algebra.Morphism.Construct.DirectProduct where

    open import Algebra.Bundles using (RawMagma; RawMonoid)
    open import Algebra.Construct.DirectProduct using (rawMagma; rawMonoid)
    open import Algebra.Morphism.Structures
      using ( module MagmaMorphisms
            ; module MonoidMorphisms
            )
    open import Data.Product as Product
      using (_,_)
    open import Level using (Level)
    open import Relation.Binary.Definitions using (Reflexive)
    import Relation.Binary.Morphism.Construct.Product as RP

    private
      variable
        a b c ℓ₁ ℓ₂ ℓ₃ : Level

    ------------------------------------------------------------------------
    -- Magmas

    module Magma (M : RawMagma a ℓ₁) (N : RawMagma b ℓ₂) where
      open MagmaMorphisms

      private
        module M = RawMagma M
        module N = RawMagma N

      module Proj₁ (refl : Reflexive M._≈_) where

        isMagmaHomomorphism : IsMagmaHomomorphism (rawMagma M N) M Product.proj₁
        isMagmaHomomorphism = record
          { isRelHomomorphism = RP.proj₁
          ; homo              = λ _ _ → refl
          }

      module Proj₂ (refl : Reflexive N._≈_) where

        isMagmaHomomorphism : IsMagmaHomomorphism (rawMagma M N) N Product.proj₂
        isMagmaHomomorphism = record
          { isRelHomomorphism = RP.proj₂
          ; homo              = λ _ _ → refl
          }

      module Pair (P : RawMagma c ℓ₃) where

        isMagmaHomomorphism : ∀ {f g} →
                              IsMagmaHomomorphism P M f →
                              IsMagmaHomomorphism P N g →
                              IsMagmaHomomorphism P (rawMagma M N) (Product.< f , g >)
        isMagmaHomomorphism F G = record
          { isRelHomomorphism = RP.< F.isRelHomomorphism , G.isRelHomomorphism >
          ; homo              = λ x y → F.homo x y , G.homo x y
          }
          where
            module F = IsMagmaHomomorphism F
            module G = IsMagmaHomomorphism G

    -- Package for export
    module Magma-Export {M : RawMagma a ℓ₁} {N : RawMagma b ℓ₂} where
      open Magma

      private
        module M = RawMagma M
        module N = RawMagma N

      module _ {refl : Reflexive M._≈_} where
        proj₁ = Proj₁.isMagmaHomomorphism M M refl

      module _ {refl : Reflexive N._≈_} where
        proj₂ = Proj₂.isMagmaHomomorphism M N refl

      module _ {P : RawMagma c ℓ₃} where
        <_,_> = Pair.isMagmaHomomorphism M N P

    ------------------------------------------------------------------------
    -- Monoids

    module Monoid (M : RawMonoid a ℓ₁) (N : RawMonoid b ℓ₂) where
      open MonoidMorphisms

      private
        module M = RawMonoid M
        module N = RawMonoid N

      module Proj₁ (refl : Reflexive M._≈_) where

        isMonoidHomomorphism : IsMonoidHomomorphism (rawMonoid M N) M Product.proj₁
        isMonoidHomomorphism = record
          { isMagmaHomomorphism = Magma.Proj₁.isMagmaHomomorphism M.rawMagma N.rawMagma refl
          ; ε-homo              = refl
          }

      module Proj₂ (refl : Reflexive N._≈_) where

        isMonoidHomomorphism : IsMonoidHomomorphism (rawMonoid M N) N Product.proj₂
        isMonoidHomomorphism = record
          { isMagmaHomomorphism = Magma.Proj₂.isMagmaHomomorphism M.rawMagma N.rawMagma refl
          ; ε-homo              = refl
          }

      module Pair (P : RawMonoid c ℓ₃) where

        private
          module P = RawMonoid P

        isMonoidHomomorphism : ∀ {f g} →
                              IsMonoidHomomorphism P M f →
                              IsMonoidHomomorphism P N g →
                              IsMonoidHomomorphism P (rawMonoid M N) (Product.< f , g >)
        isMonoidHomomorphism F G = record
          { isMagmaHomomorphism = Magma.Pair.isMagmaHomomorphism M.rawMagma N.rawMagma P.rawMagma F.isMagmaHomomorphism G.isMagmaHomomorphism
          ; ε-homo              = F.ε-homo , G.ε-homo }
          where
            module F = IsMonoidHomomorphism F
            module G = IsMonoidHomomorphism G

    -- Package for export
    module Monoid-Export {M : RawMonoid a ℓ₁} {N : RawMonoid b ℓ₂} where
      open Monoid

      private
        module M = RawMonoid M
        module N = RawMonoid N

      module _ {refl : Reflexive M._≈_} where
        proj₁ = Proj₁.isMonoidHomomorphism M M refl

      module _ {refl : Reflexive N._≈_} where
        proj₂ = Proj₂.isMonoidHomomorphism M N refl

      module _ {P : RawMonoid c ℓ₃} where
        <_,_> = Pair.isMonoidHomomorphism M N P