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