LeftCancellative _•_ = ∀ x {y z} → (x • y) ≈ (x • z) → y ≈ z
RightCancellative _•_ = ∀ {x} y z → (y • x) ≈ (z • x) → y ≈ z
AlmostLeftCancellative e _•_ = ∀ {x} y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z
AlmostRightCancellative e _•_ = ∀ {x} y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z

+-cancelˡ : ∀ {r p q} → r + p ≃ r + q → p ≃ q
+-cancelʳ : ∀ {r p q} → p + r ≃ q + r → p ≃ q