{-# OPTIONS --safe --cubical-compatible #-}
module stdlib.Algebra.Morphism.Construct.DirectProduct where

open import Algebra.Bundles using (RawMonoid)
open import Level using (Level)
open import Relation.Binary.Definitions using (Reflexive)

open import Algebra.Morphism.Construct.DirectProduct hiding (module Monoid-Export) public

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

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