------------------------------------------------------------------------
-- Properties of functions, such as associativity and commutativity
------------------------------------------------------------------------

-- These properties can (for instance) be used to define algebraic
-- structures.

open import Relation.Binary

-- The properties are specified using the equality in the given
-- setoid.

module Algebra.FunctionProperties (s : Setoid) where

open import Data.Product
open Setoid s

------------------------------------------------------------------------
-- Unary and binary operations

Op₁ : Set
Op₁ = carrier  carrier

Op₂ : Set
Op₂ = carrier  carrier  carrier

------------------------------------------------------------------------
-- Properties of operations

Associative : Op₂  Set
Associative _∙_ =  x y z  ((x  y)  z)  (x  (y  z))

Commutative : Op₂  Set
Commutative _∙_ =  x y  (x  y)  (y  x)

LeftIdentity : carrier  Op₂  Set
LeftIdentity e _∙_ =  x  (e  x)  x

RightIdentity : carrier  Op₂  Set
RightIdentity e _∙_ =  x  (x  e)  x

Identity : carrier  Op₂  Set
Identity e  = LeftIdentity e  × RightIdentity e 

LeftZero : carrier  Op₂  Set
LeftZero z _∙_ =  x  (z  x)  z

RightZero : carrier  Op₂  Set
RightZero z _∙_ =  x  (x  z)  z

Zero : carrier  Op₂  Set
Zero z  = LeftZero z  × RightZero z 

LeftInverse : carrier  Op₁  Op₂  Set
LeftInverse e _⁻¹ _∙_ =  x  (x ⁻¹  x)  e

RightInverse : carrier  Op₁  Op₂  Set
RightInverse e _⁻¹ _∙_ =  x  (x  (x ⁻¹))  e

Inverse : carrier  Op₁  Op₂  Set
Inverse e ⁻¹  = LeftInverse e ⁻¹  × RightInverse e ⁻¹ 

_DistributesOverˡ_ : Op₂  Op₂  Set
_*_ DistributesOverˡ _+_ =
   x y z  (x * (y + z))  ((x * y) + (x * z))

_DistributesOverʳ_ : Op₂  Op₂  Set
_*_ DistributesOverʳ _+_ =
   x y z  ((y + z) * x)  ((y * x) + (z * x))

_DistributesOver_ : Op₂  Op₂  Set
* DistributesOver + = (* DistributesOverˡ +) × (* DistributesOverʳ +)

_IdempotentOn_ : Op₂  carrier  Set
_∙_ IdempotentOn x = (x  x)  x

Idempotent : Op₂  Set
Idempotent  =  x   IdempotentOn x

IdempotentFun : Op₁  Set
IdempotentFun f =  x  f (f x)  f x

_Absorbs_ : Op₂  Op₂  Set
_∙_ Absorbs _∘_ =  x y  (x  (x  y))  x

Absorptive : Op₂  Op₂  Set
Absorptive   = ( Absorbs ) × ( Absorbs )

Involutive : Op₁  Set
Involutive f =  x  f (f x)  x