------------------------------------------------------------------------ -- The Agda standard library -- -- Lemmas relating algebraic definitions (such as associativity and -- commutativity) that don't require the equality relation to be a setoid. ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Algebra.Consequences.Base {a} {A : Set a} where open import Algebra.Core using (Op₁; Op₂) import Algebra.Definitions as Definitions using (Congruent₂; LeftCongruent; RightCongruent ; Selective; Idempotent; SelfInverse; Involutive) open import Data.Sum.Base using (_⊎_; reduce) open import Relation.Binary.Consequences using (mono₂⇒monoˡ; mono₂⇒monoʳ) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Definitions using (Reflexive) module Congruence {ℓ} {_∙_ : Op₂ A} (_≈_ : Rel A ℓ) (open Definitions _≈_) (cong : Congruent₂ _∙_) (refl : Reflexive _≈_) where ∙-congˡ : LeftCongruent _∙_ ∙-congˡ {x} = mono₂⇒monoˡ _ _≈_ _≈_ (refl {x = x}) cong x ∙-congʳ : RightCongruent _∙_ ∙-congʳ {x} = mono₂⇒monoʳ _≈_ _ _≈_ (refl {x = x}) cong x module _ {ℓ} {_∙_ : Op₂ A} (_≈_ : Rel A ℓ) (open Definitions _≈_) where sel⇒idem : Selective _∙_ → Idempotent _∙_ sel⇒idem sel x = reduce (sel x x) module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) (open Definitions _≈_) where reflexive∧selfInverse⇒involutive : Reflexive _≈_ → SelfInverse f → Involutive f reflexive∧selfInverse⇒involutive refl inv _ = inv refl ------------------------------------------------------------------------ -- DEPRECATED NAMES ------------------------------------------------------------------------ -- Please use the new names as continuing support for the old names is -- not guaranteed. -- Version 2.0 reflexive+selfInverse⇒involutive = reflexive∧selfInverse⇒involutive {-# WARNING_ON_USAGE reflexive+selfInverse⇒involutive "Warning: reflexive+selfInverse⇒involutive was deprecated in v2.0. Please use reflexive∧selfInverse⇒involutive instead." #-}