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