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