{-# OPTIONS --cubical-compatible --safe #-}
module Algebra.Consequences.Base
{a} {A : Set a} where
open import Algebra.Core
open import Algebra.Definitions
open import Data.Sum.Base
open import Relation.Binary.Core
open import Relation.Binary.Definitions using (Reflexive)
module _ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) where
sel⇒idem : Selective _≈_ _•_ → Idempotent _≈_ _•_
sel⇒idem sel x = reduce (sel x x)
module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where
reflexive∧selfInverse⇒involutive : Reflexive _≈_ →
SelfInverse _≈_ f →
Involutive _≈_ f
reflexive∧selfInverse⇒involutive refl inv _ = inv refl
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."
#-}