-- §──────────────────────────────────────────────────────────────────
-- Modules required for specifying parameters of this module
-- §──────────────────────────────────────────────────────────────────

import Level as L
import Relation.Binary as RB

-- §──────────────────────────────────────────────────────────────────
-- This module
-- §──────────────────────────────────────────────────────────────────

module My.Algebra.Structure.BinaryOperation {𝓁 𝓂 : L.Level} {A : Set 𝓁}
  (_≈_ : RB.Rel A 𝓂) where

-- §──────────────────────────────────────────────────────────────────
-- Other required modules
-- §──────────────────────────────────────────────────────────────────

import Algebra.FunctionProperties as AFP
import Data.Product as DP

open DP using (_×_)
open L using (_⊔_)

-- §──────────────────────────────────────────────────────────────────
-- Cancellation
-- §──────────────────────────────────────────────────────────────────

LeftCancellative : AFP.Op₂ A → Set (𝓁 ⊔ 𝓂)
LeftCancellative _∙_ = (a : A) → {x y : A} → (a ∙ x) ≈ (a ∙ y) → x ≈ y

RightCancellative : AFP.Op₂ A → Set (𝓁 ⊔ 𝓂)
RightCancellative _∙_ = (x y : A) → {a : A}  → (x ∙ a) ≈ (y ∙ a) → x ≈ y

Cancellative : AFP.Op₂ A → Set (𝓁 ⊔ 𝓂)
Cancellative _∙_ = LeftCancellative _∙_ × RightCancellative _∙_