------------------------------------------------------------------------
-- 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 )

_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ʳ +)

_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))