module My.Algebra.Structure.Predicate where

-- §──────────────────────────────────────────────────────────────────
-- Required modules
-- §──────────────────────────────────────────────────────────────────

import Algebra as A
import Algebra.FunctionProperties as AFP
import Algebra.Structures as AS
import Data.Product as DP
import Function as F
import Level as L
import Relation.Binary as RB
import Relation.Binary.EqReasoning as RBER

open DP using (_,_)
open F using (_$_)
open L using (_⊔_)

import My.Algebra.Structure.BinaryOperation as MyASBO

-- §──────────────────────────────────────────────────────────────────
-- Cancellative commutative monoid condition
-- §──────────────────────────────────────────────────────────────────

record IsCancellativeCommutativeMonoid {𝓁 𝓂 : L.Level} {A : Set 𝓁}
  (_≈_ : RB.Rel A 𝓂) (_∙_ : AFP.Op₂ A) (ε : A) : Set (𝓁 ⊔ 𝓂)
  where

    field
      isCommutativeMonoid : AS.IsCommutativeMonoid _≈_ _∙_ ε
      cancelˡ             : MyASBO.LeftCancellative _≈_ _∙_

    module ICM = AS.IsCommutativeMonoid isCommutativeMonoid

    ∙-congˡ : {a : A} → (λ x → a ∙ x) RB.Preserves _≈_ ⟶ _≈_
    ∙-congˡ = ICM.∙-cong ICM.refl

    ∙-congʳ : {a : A} → (λ x → x ∙ a) RB.Preserves _≈_ ⟶ _≈_
    ∙-congʳ p = ICM.∙-cong p ICM.refl

    assocˡ : (x y z : A) → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z))
    assocˡ = ICM.assoc

    assocʳ : (x y z : A) → (x ∙ (y ∙ z)) ≈ ((x ∙ y) ∙ z)
    assocʳ x y z = ICM.sym $ assocˡ x y z

    identityʳ : AFP.RightIdentity _≈_ ε _∙_
    identityʳ = DP.proj₂ ICM.identity

    cancelʳ : MyASBO.RightCancellative _≈_ _∙_
    cancelʳ x y {a} x∙a≈y∙a = x≈y
      where
        a∙x≈a∙y : (a ∙ x) ≈ (a ∙ y)
        a∙x≈a∙y =
          begin
            (a ∙ x) ≈⟨ ICM.comm a x ⟩
            (x ∙ a) ≈⟨ x∙a≈y∙a ⟩
            (y ∙ a) ≈⟨ ICM.comm y a ⟩
            (a ∙ y) ∎
          where
            setoid : RB.Setoid 𝓁 𝓂
            setoid = record { isEquivalence = ICM.isEquivalence }
            open RBER setoid
        x≈y = cancelˡ a a∙x≈a∙y

    cancel : MyASBO.Cancellative _≈_ _∙_
    cancel = (cancelˡ , cancelʳ)

    open ICM public