module algebra.monoid.mset where

open import level
open import algebra.monoid.core
open import algebra.monoid.morphism
open import algebra.semigroup
open import equality.core
open import hott.level

module _ {i}(M : Set i) ⦃ mM : IsMonoid M ⦄ where
  open IsMonoid ⦃ ... ⦄
  record IsMSet {j} (X : Set j) : Set (i ⊔ j) where
    constructor mk-is-mset
    field
      _◂_ : M → X → X
      ◂-hom : (m₁ m₂ : M)(x : X) → (m₁ * m₂) ◂ x ≡ m₁ ◂ (m₂ ◂ x)
      ◂-id : (x : X) → e ◂ x ≡ x
      mset-level : h  X

  open IsMSet ⦃ ... ⦄

  module _ {j k}
           {X : Set j} ⦃ xM : IsMSet X ⦄
           {Y : Set k} ⦃ yM : IsMSet Y ⦄ where
    IsMSetMorphism : (X → Y) → Set (i ⊔ j ⊔ k)
    IsMSetMorphism f = (m : M)(x : X) → f (m ◂ x) ≡ m ◂ f x

    is-mset-morphism-level : h  Y → (f : X → Y)
      → h  (IsMSetMorphism f)
    is-mset-morphism-level hY f = Π-level λ m → Π-level λ x → hY _ _