module My.Algebra.Structure.Object where
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
record CancellativeCommutativeMonoid (𝓁 𝓂 : L.Level) : Set (L.suc (𝓁 ⊔ 𝓂))
where
infixl 7 _∙_
infix 4 _≈_
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)