{-# 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ʳ≡ )