module My.Algebra.Structure.Predicate where
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
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