open import Relation.Binary
module Algebra.FunctionProperties (s : Setoid) where
open import Data.Product
open Setoid s
Op₁ : Set
Op₁ = carrier → carrier
Op₂ : Set
Op₂ = carrier → carrier → carrier
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