------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of functions, such as associativity and commutativity
------------------------------------------------------------------------
 
-- The contents of this module should be accessed via `Algebra`, unless
-- you want to parameterise it via the equality relation.
 
-- Note that very few of the element arguments are made implicit here,
-- as we do not assume that the Agda can infer either the right or left
-- argument of the binary operators. This is despite the fact that the
-- library defines most of its concrete operators (e.g. in
-- `Data.Nat.Base`) as being left-biased.
 
{-# OPTIONS --cubical-compatible --safe #-}
 
open import Relation.Binary.Core using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
open import Relation.Nullary.Negation.Core using (¬_)
 
module Algebra.Definitions
  {a ℓ} {A : Set a}   -- The underlying set
  (_≈_ : Rel A ℓ)     -- The underlying equality
  where
 
open import Algebra.Core using (Op₁; Op₂)
open import Data.Product.Base using (_×_; ∃-syntax)
open import Data.Sum.Base using (_⊎_)
 
------------------------------------------------------------------------
-- Properties of operations
 
Congruent₁ : Op₁ A → Set _
Congruent₁ f = f Preserves _≈_ ⟶ _≈_
 
Congruent₂ : Op₂ A → Set _
Congruent₂ ∙ = ∙ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
 
LeftCongruent : Op₂ A → Set _
LeftCongruent _∙_ = ∀ {x} → (x ∙_) Preserves _≈_ ⟶ _≈_
 
RightCongruent : Op₂ A → Set _
RightCongruent _∙_ = ∀ {x} → (_∙ x) Preserves _≈_ ⟶ _≈_
 
Associative : Op₂ A → Set _
Associative _∙_ = ∀ x y z → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z))
 
Commutative : Op₂ A → Set _
Commutative _∙_ = ∀ x y → (x ∙ y) ≈ (y ∙ x)
 
LeftIdentity : A → Op₂ A → Set _
LeftIdentity e _∙_ = ∀ x → (e ∙ x) ≈ x
 
RightIdentity : A → Op₂ A → Set _
RightIdentity e _∙_ = ∀ x → (x ∙ e) ≈ x
 
Identity : A → Op₂ A → Set _
Identity e ∙ = (LeftIdentity e ∙) × (RightIdentity e ∙)
 
LeftZero : A → Op₂ A → Set _
LeftZero z _∙_ = ∀ x → (z ∙ x) ≈ z
 
RightZero : A → Op₂ A → Set _
RightZero z _∙_ = ∀ x → (x ∙ z) ≈ z
 
Zero : A → Op₂ A → Set _
Zero z ∙ = (LeftZero z ∙) × (RightZero z ∙)
 
LeftInverse : A → Op₁ A → Op₂ A → Set _
LeftInverse e _⁻¹ _∙_ = ∀ x → ((x ⁻¹) ∙ x) ≈ e
 
RightInverse : A → Op₁ A → Op₂ A → Set _
RightInverse e _⁻¹ _∙_ = ∀ x → (x ∙ (x ⁻¹)) ≈ e
 
Inverse : A → Op₁ A → Op₂ A → Set _
Inverse e ⁻¹ ∙ = (LeftInverse e ⁻¹) ∙ × (RightInverse e ⁻¹ ∙)
 
-- For structures in which not every element has an inverse (e.g. Fields)
LeftInvertible : A → Op₂ A → A → Set _
LeftInvertible e _∙_ x = ∃[ x⁻¹ ] (x⁻¹ ∙ x) ≈ e
 
RightInvertible : A → Op₂ A → A → Set _
RightInvertible e _∙_ x = ∃[ x⁻¹ ] (x ∙ x⁻¹) ≈ e
 
-- NB: this is not quite the same as
-- LeftInvertible e ∙ x × RightInvertible e ∙ x
-- since the left and right inverses have to coincide.
Invertible : A → Op₂ A → A → Set _
Invertible e _∙_ x = ∃[ x⁻¹ ] (x⁻¹ ∙ x) ≈ e × (x ∙ x⁻¹) ≈ e
 
LeftConical : A → Op₂ A → Set _
LeftConical e _∙_ = ∀ x y → (x ∙ y) ≈ e → x ≈ e
 
RightConical : A → Op₂ A → Set _
RightConical e _∙_ = ∀ x y → (x ∙ y) ≈ e → y ≈ e
 
Conical : A → Op₂ A → Set _
Conical e ∙ = (LeftConical e ∙) × (RightConical e ∙)
 
infix  _DistributesOverˡ_ _DistributesOverʳ_ _DistributesOver_
 
_DistributesOverˡ_ : Op₂ A → Op₂ A → Set _
_*_ DistributesOverˡ _+_ =
  ∀ x y z → (x * (y + z)) ≈ ((x * y) + (x * z))
 
_DistributesOverʳ_ : Op₂ A → Op₂ A → Set _
_*_ DistributesOverʳ _+_ =
  ∀ x y z → ((y + z) * x) ≈ ((y * x) + (z * x))
 
_DistributesOver_ : Op₂ A → Op₂ A → Set _
* DistributesOver + = (* DistributesOverˡ +) × (* DistributesOverʳ +)
 
infix  _MiddleFourExchange_ _IdempotentOn_ _Absorbs_
 
_MiddleFourExchange_ : Op₂ A → Op₂ A → Set _
_*_ MiddleFourExchange _+_ =
  ∀ w x y z → ((w + x) * (y + z)) ≈ ((w + y) * (x + z))
 
_IdempotentOn_ : Op₂ A → A → Set _
_∙_ IdempotentOn x = (x ∙ x) ≈ x
 
Idempotent : Op₂ A → Set _
Idempotent ∙ = ∀ x → ∙ IdempotentOn x
 
IdempotentFun : Op₁ A → Set _
IdempotentFun f = ∀ x → f (f x) ≈ f x
 
Selective : Op₂ A → Set _
Selective _∙_ = ∀ x y → (x ∙ y) ≈ x ⊎ (x ∙ y) ≈ y
 
_Absorbs_ : Op₂ A → Op₂ A → Set _
_∙_ Absorbs _∘_ = ∀ x y → (x ∙ (x ∘ y)) ≈ x
 
Absorptive : Op₂ A → Op₂ A → Set _
Absorptive ∙ ∘ = (∙ Absorbs ∘) × (∘ Absorbs ∙)
 
SelfInverse : Op₁ A → Set _
SelfInverse f = ∀ {x y} → f x ≈ y → f y ≈ x
 
Involutive : Op₁ A → Set _
Involutive f = ∀ x → f (f x) ≈ x
 
LeftCancellative : Op₂ A → Set _
LeftCancellative _•_ = ∀ x y z → (x • y) ≈ (x • z) → y ≈ z
 
RightCancellative : Op₂ A → Set _
RightCancellative _•_ = ∀ x y z → (y • x) ≈ (z • x) → y ≈ z
 
Cancellative : Op₂ A → Set _
Cancellative _•_ = (LeftCancellative _•_) × (RightCancellative _•_)
 
AlmostLeftCancellative : A → Op₂ A → Set _
AlmostLeftCancellative e _•_ = ∀ x y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z
 
AlmostRightCancellative : A → Op₂ A → Set _
AlmostRightCancellative e _•_ = ∀ x y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z
 
AlmostCancellative : A → Op₂ A → Set _
AlmostCancellative e _•_ = AlmostLeftCancellative e _•_ × AlmostRightCancellative e _•_
 
Interchangable : Op₂ A → Op₂ A → Set _
Interchangable _∘_ _∙_ = ∀ w x y z → ((w ∙ x) ∘ (y ∙ z)) ≈ ((w ∘ y) ∙ (x ∘ z))
 
LeftDividesˡ : Op₂ A → Op₂ A → Set _
LeftDividesˡ _∙_  _\\_ = ∀ x y → (x ∙ (x \\ y)) ≈ y
 
LeftDividesʳ : Op₂ A → Op₂ A → Set _
LeftDividesʳ _∙_ _\\_ = ∀ x y → (x \\ (x ∙ y)) ≈ y
 
RightDividesˡ : Op₂ A → Op₂ A → Set _
RightDividesˡ _∙_ _//_ = ∀ x y → ((y // x) ∙ x) ≈ y
 
RightDividesʳ : Op₂ A → Op₂ A → Set _
RightDividesʳ _∙_ _//_ = ∀ x y → ((y ∙ x) // x) ≈ y
 
LeftDivides : Op₂ A → Op₂ A → Set _
LeftDivides ∙ \\ = (LeftDividesˡ ∙ \\) × (LeftDividesʳ ∙ \\)
 
RightDivides : Op₂ A → Op₂ A → Set _
RightDivides ∙ // = (RightDividesˡ ∙ //) × (RightDividesʳ ∙ //)
 
StarRightExpansive : A → Op₂ A → Op₂ A → Op₁ A → Set _
StarRightExpansive e _+_ _∙_ _* = ∀ x → (e + (x ∙ (x *))) ≈ (x *)
 
StarLeftExpansive : A → Op₂ A → Op₂ A → Op₁ A → Set _
StarLeftExpansive e _+_ _∙_ _* = ∀ x →  (e + ((x *) ∙ x)) ≈ (x *)
 
StarExpansive : A → Op₂ A → Op₂ A → Op₁ A → Set _
StarExpansive e _+_ _∙_ _* = (StarLeftExpansive e _+_ _∙_ _*) × (StarRightExpansive e _+_ _∙_ _*)
 
StarLeftDestructive : Op₂ A → Op₂ A → Op₁ A → Set _
StarLeftDestructive _+_ _∙_ _* = ∀ a b x → (b + (a ∙ x)) ≈ x → ((a *) ∙ b) ≈ x
 
StarRightDestructive : Op₂ A → Op₂ A → Op₁ A → Set _
StarRightDestructive _+_ _∙_ _* = ∀ a b x → (b + (x ∙ a)) ≈ x → (b ∙ (a *)) ≈ x
 
StarDestructive : Op₂ A → Op₂ A → Op₁ A → Set _
StarDestructive _+_ _∙_ _* = (StarLeftDestructive _+_ _∙_ _*) × (StarRightDestructive _+_ _∙_ _*)
 
LeftAlternative : Op₂ A → Set _
LeftAlternative _∙_ = ∀ x y  →  ((x ∙ x) ∙ y) ≈ (x ∙ (x ∙ y))
 
RightAlternative : Op₂ A → Set _
RightAlternative _∙_ = ∀ x y → (x ∙ (y ∙ y)) ≈ ((x ∙ y) ∙ y)
 
Alternative : Op₂ A → Set _
Alternative _∙_ = (LeftAlternative _∙_ ) × (RightAlternative _∙_)
 
Flexible : Op₂ A → Set _
Flexible _∙_ = ∀ x y → ((x ∙ y) ∙ x) ≈ (x ∙ (y ∙ x))
 
Medial : Op₂ A → Set _
Medial _∙_ = ∀ x y u z → ((x ∙ y) ∙ (u ∙ z)) ≈ ((x ∙ u) ∙ (y ∙ z))
 
LeftSemimedial : Op₂ A → Set _
LeftSemimedial _∙_ = ∀ x y z → ((x ∙ x) ∙ (y ∙ z)) ≈ ((x ∙ y) ∙ (x ∙ z))
 
RightSemimedial : Op₂ A → Set _
RightSemimedial _∙_ = ∀ x y z → ((y ∙ z) ∙ (x ∙ x)) ≈ ((y ∙ x) ∙ (z ∙ x))
 
Semimedial : Op₂ A → Set _
Semimedial _∙_ = (LeftSemimedial _∙_) × (RightSemimedial _∙_)
 
LeftBol : Op₂ A → Set _
LeftBol _∙_ = ∀ x y z → (x ∙ (y ∙ (x ∙ z))) ≈ ((x ∙ (y ∙ x)) ∙ z )
 
RightBol : Op₂ A → Set _
RightBol _∙_ = ∀ x y z → (((z ∙ x) ∙ y) ∙ x) ≈ (z ∙ ((x ∙ y) ∙ x))
 
MiddleBol : Op₂ A → Op₂ A  → Op₂ A  → Set _
MiddleBol _∙_ _\\_ _//_ = ∀ x y z → (x ∙ ((y ∙ z) \\ x)) ≈ ((x // z) ∙ (y \\ x))
 
Identical : Op₂ A → Set _
Identical _∙_ = ∀ x y z → ((z ∙ x) ∙ (y ∙ z)) ≈ (z ∙ ((x ∙ y) ∙ z))