module My.Algebra.Structure.Object where

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

import Algebra as A
import Algebra.FunctionProperties as AFP
import Algebra.Structures as AS
import Function as F
import Level as L
import Relation.Binary as RB

open L using (_⊔_)

import My.Algebra.Structure.Predicate as MyASP

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

record CancellativeCommutativeMonoid (𝓁 𝓂 : L.Level) : Set (L.suc (𝓁 ⊔ 𝓂))
  where

    infixl  _∙_
    infix   _≈_

    field
      Carrier                         : Set 𝓁
      _≈_                             : RB.Rel Carrier 𝓂
      _∙_                             : AFP.Op₂ Carrier
      ε                               : Carrier
      isCancellativeCommutativeMonoid : MyASP.IsCancellativeCommutativeMonoid
                                        _≈_ _∙_ ε

    open MyASP.IsCancellativeCommutativeMonoid isCancellativeCommutativeMonoid
      public

    commutativeMonoid : A.CommutativeMonoid 𝓁 𝓂
    commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }

    open A.CommutativeMonoid commutativeMonoid public
      using (setoid ; semigroup ; rawMonoid ; monoid)