{-# OPTIONS --cubical-compatible #-}
module Class.Semigroup.Core where

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

record Semigroup (A : Type ℓ) : Type ℓ where
  infixr  _◇_ _<>_
  field _◇_ : A → A → A
  _<>_ = _◇_
open Semigroup ⦃...⦄ public

module _ (A : Type ℓ) ⦃ _ : Semigroup A ⦄ where
  record SemigroupLaws ⦃ _ : ISetoid A ⦄ ⦃ _ : SetoidLaws A ⦄ : Type (ℓ ⊔ relℓ) where
    open Alg _≈_
    field ◇-comm   : Commutative _◇_
          ◇-assocʳ : Associative _◇_

    ◇-assocˡ : ∀ (x y z : A) → (x ◇ (y ◇ z)) ≈ ((x ◇ y) ◇ z)
    ◇-assocˡ x y z = ≈-sym (◇-assocʳ x y z)

  instance _ = mkISetoid≡; _ = mkSetoidLaws≡

  SemigroupLaws≡ : Type ℓ
  SemigroupLaws≡ = SemigroupLaws

open SemigroupLaws ⦃...⦄ public

module _ ⦃ _ : Semigroup A ⦄ ⦃ _ : SemigroupLaws≡ A ⦄ where

  instance _ = mkISetoid≡; _ = mkSetoidLaws≡

  open SemigroupLaws it public
    renaming (◇-comm to ◇-comm≡; ◇-assocʳ to ◇-assocʳ≡; ◇-assocˡ to ◇-assocˡ≡)