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