Source code on Github
{-# OPTIONS --cubical-compatible #-}
module Class.Monoid.Core where

open import Class.Prelude
open import Class.Semigroup
open import Class.Setoid.Core

record Monoid (A : Type )  _ : Semigroup A  : Type  where
  field ε : A
open Monoid ⦃...⦄ public

module _ (A : Type )  _ : Semigroup A   _ : Monoid A  where

  record MonoidLaws  _ : ISetoid A  : Type (  relℓ) where
    open Alg _≈_
    field ε-identity : Identity ε _◇_
    ε-identityˡ = LeftIdentity  ε _◇_  ε-identity .proj₁
    ε-identityʳ = RightIdentity ε _◇_  ε-identity .proj₂

  MonoidLaws≡ : Type _
  MonoidLaws≡ = MonoidLaws
    where instance _ = mkISetoid≡; _ = mkSetoidLaws≡

open MonoidLaws ⦃...⦄ public

module _  _ : Semigroup A   _ : Monoid A   _ : MonoidLaws≡ A  where
  instance _ = mkISetoid≡; _ = mkSetoidLaws≡
  open MonoidLaws it public
    renaming ( ε-identity to ε-identity≡
             ; ε-identityˡ to ε-identityˡ≡; ε-identityʳ to ε-identityʳ≡ )