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

{-# OPTIONS --without-K --safe #-}

open import Relation.Binary.Core
open import Relation.Nullary using (¬_)

module Algebra.Definitions
  {a } {A : Set a}   -- The underlying set
  (_≈_ : Rel A )     -- The underlying equality
  where

open import Algebra.Core
open import Data.Product
open import Data.Sum.Base

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

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

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

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