    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Relations between properties of functions, such as associativity and
    -- commutativity, when the underlying relation is a setoid
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    open import Relation.Binary.Bundles using (Setoid)
    open import Relation.Binary.Definitions
      using (Substitutive; Symmetric; Total)

    module Algebra.Consequences.Setoid {a ℓ} (S : Setoid a ℓ) where

    import Algebra.Consequences.Base as Base
    open import Algebra.Core
    open import Data.Sum.Base using (inj₁; inj₂)
    open import Data.Product.Base using (_,_)
    open import Function.Base using (_$_; id; _∘_)
    open import Function.Definitions
    import Relation.Binary.Consequences as Bin
    open import Relation.Binary.Core using (Rel)
    open import Relation.Unary using (Pred)

    open Setoid S renaming (Carrier to A)
    open import Algebra.Definitions _≈_
    open import Relation.Binary.Reasoning.Setoid S

    ------------------------------------------------------------------------
    -- Re-exports

    -- Export base lemmas that don't require the setoid

    open Base public
      hiding (module Congruence)

    -- Export congruence lemmas using reflexivity

    module Congruence {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where

      open Base.Congruence _≈_ cong refl public

    ------------------------------------------------------------------------
    -- MiddleFourExchange

    module _ {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where

      open Congruence cong

      comm∧assoc⇒middleFour : Commutative _∙_ → Associative _∙_ →
                              _∙_ MiddleFourExchange _∙_
      comm∧assoc⇒middleFour comm assoc w x y z = begin
        (w ∙ x) ∙ (y ∙ z) ≈⟨ assoc w x (y ∙ z) ⟩
        w ∙ (x ∙ (y ∙ z)) ≈⟨ ∙-congˡ (assoc x y z) ⟨
        w ∙ ((x ∙ y) ∙ z) ≈⟨ ∙-congˡ (∙-congʳ (comm x y)) ⟩
        w ∙ ((y ∙ x) ∙ z) ≈⟨ ∙-congˡ (assoc y x z) ⟩
        w ∙ (y ∙ (x ∙ z)) ≈⟨ assoc w y (x ∙ z) ⟨
        (w ∙ y) ∙ (x ∙ z) ∎

      identity∧middleFour⇒assoc : {e : A} → Identity e _∙_ →
                                  _∙_ MiddleFourExchange _∙_ →
                                  Associative _∙_
      identity∧middleFour⇒assoc {e} (identityˡ , identityʳ) middleFour x y z = begin
        (x ∙ y) ∙ z       ≈⟨ ∙-congˡ (identityˡ z) ⟨
        (x ∙ y) ∙ (e ∙ z) ≈⟨ middleFour x y e z ⟩
        (x ∙ e) ∙ (y ∙ z) ≈⟨ ∙-congʳ (identityʳ x) ⟩
        x ∙ (y ∙ z)       ∎

      identity∧middleFour⇒comm : {_+_ : Op₂ A} {e : A} → Identity e _+_ →
                                 _∙_ MiddleFourExchange _+_ →
                                 Commutative _∙_
      identity∧middleFour⇒comm {_+_} {e} (identityˡ , identityʳ) middleFour x y
        = begin
        x ∙ y             ≈⟨ cong (identityˡ x) (identityʳ y) ⟨
        (e + x) ∙ (y + e) ≈⟨ middleFour e x y e ⟩
        (e + y) ∙ (x + e) ≈⟨ cong (identityˡ y) (identityʳ x) ⟩
        y ∙ x             ∎

    ------------------------------------------------------------------------
    -- SelfInverse

    module _ {f : Op₁ A} (self : SelfInverse f) where

      selfInverse⇒involutive : Involutive f
      selfInverse⇒involutive = reflexive∧selfInverse⇒involutive _≈_ refl self

      selfInverse⇒congruent : Congruent _≈_ _≈_ f
      selfInverse⇒congruent {x} {y} x≈y = sym (self (begin
        f (f x) ≈⟨ selfInverse⇒involutive x ⟩
        x       ≈⟨ x≈y ⟩
        y       ∎))

      selfInverse⇒inverseᵇ : Inverseᵇ _≈_ _≈_ f f
      selfInverse⇒inverseᵇ = self ∘ sym , self ∘ sym

      selfInverse⇒surjective : Surjective _≈_ _≈_ f
      selfInverse⇒surjective y = f y , self ∘ sym

      selfInverse⇒injective : Injective _≈_ _≈_ f
      selfInverse⇒injective {x} {y} x≈y = begin
        x       ≈⟨ self x≈y ⟨
        f (f y) ≈⟨ selfInverse⇒involutive y ⟩
        y       ∎

      selfInverse⇒bijective : Bijective _≈_ _≈_ f
      selfInverse⇒bijective = selfInverse⇒injective , selfInverse⇒surjective

    ------------------------------------------------------------------------
    -- Magma-like structures

    module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) where

      comm∧cancelˡ⇒cancelʳ : LeftCancellative _∙_ → RightCancellative _∙_
      comm∧cancelˡ⇒cancelʳ cancelˡ x y z eq = cancelˡ x y z $ begin
        x ∙ y ≈⟨ comm x y ⟩
        y ∙ x ≈⟨ eq ⟩
        z ∙ x ≈⟨ comm z x ⟩
        x ∙ z ∎

      comm∧cancelʳ⇒cancelˡ : RightCancellative _∙_ → LeftCancellative _∙_
      comm∧cancelʳ⇒cancelˡ cancelʳ x y z eq = cancelʳ x y z $ begin
        y ∙ x ≈⟨ comm y x ⟩
        x ∙ y ≈⟨ eq ⟩
        x ∙ z ≈⟨ comm x z ⟩
        z ∙ x ∎

    ------------------------------------------------------------------------
    -- Monoid-like structures

    module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) {e : A} where

      comm∧idˡ⇒idʳ : LeftIdentity e _∙_ → RightIdentity e _∙_
      comm∧idˡ⇒idʳ idˡ x = begin
        x ∙ e ≈⟨ comm x e ⟩
        e ∙ x ≈⟨ idˡ x ⟩
        x     ∎

      comm∧idʳ⇒idˡ : RightIdentity e _∙_ → LeftIdentity e _∙_
      comm∧idʳ⇒idˡ idʳ x = begin
        e ∙ x ≈⟨ comm e x ⟩
        x ∙ e ≈⟨ idʳ x ⟩
        x     ∎

      comm∧idˡ⇒id : LeftIdentity e _∙_ → Identity e _∙_
      comm∧idˡ⇒id idˡ = idˡ , comm∧idˡ⇒idʳ idˡ

      comm∧idʳ⇒id : RightIdentity e _∙_ → Identity e _∙_
      comm∧idʳ⇒id idʳ = comm∧idʳ⇒idˡ idʳ , idʳ

      comm∧zeˡ⇒zeʳ : LeftZero e _∙_ → RightZero e _∙_
      comm∧zeˡ⇒zeʳ zeˡ x = begin
        x ∙ e ≈⟨ comm x e ⟩
        e ∙ x ≈⟨ zeˡ x ⟩
        e     ∎

      comm∧zeʳ⇒zeˡ : RightZero e _∙_ → LeftZero e _∙_
      comm∧zeʳ⇒zeˡ zeʳ x = begin
        e ∙ x ≈⟨ comm e x ⟩
        x ∙ e ≈⟨ zeʳ x ⟩
        e     ∎

      comm∧zeˡ⇒ze : LeftZero e _∙_ → Zero e _∙_
      comm∧zeˡ⇒ze zeˡ = zeˡ , comm∧zeˡ⇒zeʳ zeˡ

      comm∧zeʳ⇒ze : RightZero e _∙_ → Zero e _∙_
      comm∧zeʳ⇒ze zeʳ = comm∧zeʳ⇒zeˡ zeʳ , zeʳ

      comm∧almostCancelˡ⇒almostCancelʳ : AlmostLeftCancellative e _∙_ →
                                         AlmostRightCancellative e _∙_
      comm∧almostCancelˡ⇒almostCancelʳ cancelˡ-nonZero x y z x≉e yx≈zx =
        cancelˡ-nonZero x y z x≉e $ begin
          x ∙ y ≈⟨ comm x y ⟩
          y ∙ x ≈⟨ yx≈zx ⟩
          z ∙ x ≈⟨ comm z x ⟩
          x ∙ z ∎

      comm∧almostCancelʳ⇒almostCancelˡ : AlmostRightCancellative e _∙_ →
                                         AlmostLeftCancellative e _∙_
      comm∧almostCancelʳ⇒almostCancelˡ cancelʳ-nonZero x y z x≉e xy≈xz =
        cancelʳ-nonZero x y z x≉e $ begin
          y ∙ x ≈⟨ comm y x ⟩
          x ∙ y ≈⟨ xy≈xz ⟩
          x ∙ z ≈⟨ comm x z ⟩
          z ∙ x ∎

    ------------------------------------------------------------------------
    -- Group-like structures

    module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (comm : Commutative _∙_) where

      comm∧invˡ⇒invʳ : LeftInverse e _⁻¹ _∙_ → RightInverse e _⁻¹ _∙_
      comm∧invˡ⇒invʳ invˡ x = begin
        x ∙ (x ⁻¹) ≈⟨ comm x (x ⁻¹) ⟩
        (x ⁻¹) ∙ x ≈⟨ invˡ x ⟩
        e          ∎

      comm∧invˡ⇒inv : LeftInverse e _⁻¹ _∙_ → Inverse e _⁻¹ _∙_
      comm∧invˡ⇒inv invˡ = invˡ , comm∧invˡ⇒invʳ invˡ

      comm∧invʳ⇒invˡ : RightInverse e _⁻¹ _∙_ → LeftInverse e _⁻¹ _∙_
      comm∧invʳ⇒invˡ invʳ x = begin
        (x ⁻¹) ∙ x ≈⟨ comm (x ⁻¹) x ⟩
        x ∙ (x ⁻¹) ≈⟨ invʳ x ⟩
        e          ∎

      comm∧invʳ⇒inv : RightInverse e _⁻¹ _∙_ → Inverse e _⁻¹ _∙_
      comm∧invʳ⇒inv invʳ = comm∧invʳ⇒invˡ invʳ , invʳ

    module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _∙_) where

      open Congruence cong

      assoc∧id∧invʳ⇒invˡ-unique : Associative _∙_ →
                                  Identity e _∙_ → RightInverse e _⁻¹ _∙_ →
                                  ∀ x y → (x ∙ y) ≈ e → x ≈ (y ⁻¹)
      assoc∧id∧invʳ⇒invˡ-unique assoc (idˡ , idʳ) invʳ x y eq = begin
        x                ≈⟨ idʳ x ⟨
        x ∙ e            ≈⟨ ∙-congˡ (invʳ y) ⟨
        x ∙ (y ∙ (y ⁻¹)) ≈⟨ assoc x y (y ⁻¹) ⟨
        (x ∙ y) ∙ (y ⁻¹) ≈⟨ ∙-congʳ eq ⟩
        e ∙ (y ⁻¹)       ≈⟨ idˡ (y ⁻¹) ⟩
        y ⁻¹             ∎

      assoc∧id∧invˡ⇒invʳ-unique : Associative _∙_ →
                                  Identity e _∙_ → LeftInverse e _⁻¹ _∙_ →
                                  ∀ x y → (x ∙ y) ≈ e → y ≈ (x ⁻¹)
      assoc∧id∧invˡ⇒invʳ-unique assoc (idˡ , idʳ) invˡ x y eq = begin
        y                ≈⟨ idˡ y ⟨
        e ∙ y            ≈⟨ ∙-congʳ (invˡ x) ⟨
        ((x ⁻¹) ∙ x) ∙ y ≈⟨ assoc (x ⁻¹) x y ⟩
        (x ⁻¹) ∙ (x ∙ y) ≈⟨ ∙-congˡ eq ⟩
        (x ⁻¹) ∙ e       ≈⟨ idʳ (x ⁻¹) ⟩
        x ⁻¹             ∎

    ------------------------------------------------------------------------
    -- Bisemigroup-like structures

    module _ {_∙_ _◦_ : Op₂ A}
             (◦-cong : Congruent₂ _◦_)
             (∙-comm : Commutative _∙_)
             where

      open Congruence ◦-cong renaming (∙-congˡ to ◦-congˡ)

      comm∧distrˡ⇒distrʳ :  _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOverʳ _◦_
      comm∧distrˡ⇒distrʳ distrˡ x y z = begin
        (y ◦ z) ∙ x       ≈⟨ ∙-comm (y ◦ z) x ⟩
        x ∙ (y ◦ z)       ≈⟨ distrˡ x y z ⟩
        (x ∙ y) ◦ (x ∙ z) ≈⟨ ◦-cong (∙-comm x y) (∙-comm x z) ⟩
        (y ∙ x) ◦ (z ∙ x) ∎

      comm∧distrʳ⇒distrˡ : _∙_ DistributesOverʳ _◦_ → _∙_ DistributesOverˡ _◦_
      comm∧distrʳ⇒distrˡ distrˡ x y z = begin
        x ∙ (y ◦ z)       ≈⟨ ∙-comm x (y ◦ z) ⟩
        (y ◦ z) ∙ x       ≈⟨ distrˡ x y z ⟩
        (y ∙ x) ◦ (z ∙ x) ≈⟨ ◦-cong (∙-comm y x) (∙-comm z x) ⟩
        (x ∙ y) ◦ (x ∙ z) ∎

      comm∧distrˡ⇒distr :  _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOver _◦_
      comm∧distrˡ⇒distr distrˡ = distrˡ , comm∧distrˡ⇒distrʳ distrˡ

      comm∧distrʳ⇒distr :  _∙_ DistributesOverʳ _◦_ → _∙_ DistributesOver _◦_
      comm∧distrʳ⇒distr distrʳ = comm∧distrʳ⇒distrˡ distrʳ , distrʳ

      comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y ∙ z)) ≈ ((x ◦ y) ∙ (x ◦ z)))
      comm⇒sym[distribˡ] x {y} {z} prf = begin
        x ◦ (z ∙ y)       ≈⟨ ◦-congˡ (∙-comm z y) ⟩
        x ◦ (y ∙ z)       ≈⟨ prf ⟩
        (x ◦ y) ∙ (x ◦ z) ≈⟨ ∙-comm (x ◦ y) (x ◦ z) ⟩
        (x ◦ z) ∙ (x ◦ y) ∎

    module _ {_∙_ _◦_ : Op₂ A}
             (∙-cong  : Congruent₂ _∙_)
             (∙-assoc : Associative _∙_)
             (◦-comm  : Commutative _◦_)
             where

      open Congruence ∙-cong

      distrib∧absorbs⇒distribˡ : _∙_ Absorbs _◦_ →
                                 _◦_ Absorbs _∙_ →
                                 _◦_ DistributesOver _∙_ →
                                 _∙_ DistributesOverˡ _◦_
      distrib∧absorbs⇒distribˡ ∙-absorbs-◦ ◦-absorbs-∙ (◦-distribˡ-∙ , ◦-distribʳ-∙) x y z = begin
        x ∙ (y ◦ z)                    ≈⟨ ∙-congʳ (∙-absorbs-◦ _ _) ⟨
        (x ∙ (x ◦ y)) ∙ (y ◦ z)        ≈⟨  ∙-congʳ (∙-congˡ (◦-comm _ _)) ⟩
        (x ∙ (y ◦ x)) ∙ (y ◦ z)        ≈⟨  ∙-assoc _ _ _ ⟩
        x ∙ ((y ◦ x) ∙ (y ◦ z))        ≈⟨ ∙-congˡ (◦-distribˡ-∙ _ _ _) ⟨
        x ∙ (y ◦ (x ∙ z))              ≈⟨ ∙-congʳ (◦-absorbs-∙ _ _) ⟨
        (x ◦ (x ∙ z)) ∙ (y ◦ (x ∙ z))  ≈⟨ ◦-distribʳ-∙ _ _ _ ⟨
        (x ∙ y) ◦ (x ∙ z)              ∎

    ------------------------------------------------------------------------
    -- Ring-like structures

    module _ {_+_ _*_ : Op₂ A}
             {_⁻¹ : Op₁ A} {0# : A}
             (+-cong : Congruent₂ _+_)
             (*-cong : Congruent₂ _*_)
             where

      open Congruence +-cong renaming (∙-congˡ to +-congˡ; ∙-congʳ to +-congʳ)

      open Congruence *-cong renaming (∙-congˡ to *-congˡ; ∙-congʳ to *-congʳ)

      assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ : Associative _+_ → _*_ DistributesOverʳ _+_ →
                                    RightIdentity 0# _+_ → RightInverse 0# _⁻¹ _+_ →
                                    LeftZero 0# _*_
      assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ +-assoc distribʳ idʳ invʳ  x = begin
        0# * x                                 ≈⟨ idʳ _ ⟨
        (0# * x) + 0#                          ≈⟨ +-congˡ (invʳ _) ⟨
        (0# * x) + ((0# * x)  + ((0# * x)⁻¹))  ≈⟨ +-assoc _ _ _ ⟨
        ((0# * x) +  (0# * x)) + ((0# * x)⁻¹)  ≈⟨ +-congʳ (distribʳ _ _ _) ⟨
        ((0# + 0#) * x) + ((0# * x)⁻¹)         ≈⟨ +-congʳ (*-congʳ (idʳ _)) ⟩
        (0# * x) + ((0# * x)⁻¹)                ≈⟨ invʳ _ ⟩
        0#                                     ∎

      assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ : Associative _+_ → _*_ DistributesOverˡ _+_ →
                                    RightIdentity 0# _+_ → RightInverse 0# _⁻¹ _+_ →
                                    RightZero 0# _*_
      assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ +-assoc distribˡ idʳ invʳ  x = begin
         x * 0#                                ≈⟨ idʳ _ ⟨
         (x * 0#) + 0#                         ≈⟨ +-congˡ (invʳ _) ⟨
         (x * 0#) + ((x * 0#) + ((x * 0#)⁻¹))  ≈⟨ +-assoc _ _ _ ⟨
         ((x * 0#) + (x * 0#)) + ((x * 0#)⁻¹)  ≈⟨ +-congʳ (distribˡ _ _ _) ⟨
         (x * (0# + 0#)) + ((x * 0#)⁻¹)        ≈⟨ +-congʳ (*-congˡ (idʳ _)) ⟩
         ((x * 0#) + ((x * 0#)⁻¹))             ≈⟨ invʳ _ ⟩
         0#                                    ∎

    ------------------------------------------------------------------------
    -- Without Loss of Generality

    module _ {p} {f : Op₂ A} {P : Pred A p}
             (≈-subst : Substitutive _≈_ p)
             (comm : Commutative f)
             where

      subst∧comm⇒sym : Symmetric (λ a b → P (f a b))
      subst∧comm⇒sym = ≈-subst P (comm _ _)

      wlog : ∀ {r} {_R_ : Rel _ r} → Total _R_ →
             (∀ a b → a R b → P (f a b)) →
             ∀ a b → P (f a b)
      wlog r-total = Bin.wlog r-total subst∧comm⇒sym

    ------------------------------------------------------------------------
    -- DEPRECATED NAMES
    ------------------------------------------------------------------------
    -- Please use the new names as continuing support for the old names is
    -- not guaranteed.

    -- Version 2.0

    comm+assoc⇒middleFour = comm∧assoc⇒middleFour
    {-# WARNING_ON_USAGE comm+assoc⇒middleFour
    "Warning: comm+assoc⇒middleFour was deprecated in v2.0.
    Please use comm∧assoc⇒middleFour instead."
    #-}
    identity+middleFour⇒assoc = identity∧middleFour⇒assoc
    {-# WARNING_ON_USAGE identity+middleFour⇒assoc
    "Warning: identity+middleFour⇒assoc was deprecated in v2.0.
    Please use identity∧middleFour⇒assoc instead."
    #-}
    identity+middleFour⇒comm = identity∧middleFour⇒comm
    {-# WARNING_ON_USAGE identity+middleFour⇒comm
    "Warning: identity+middleFour⇒comm was deprecated in v2.0.
    Please use identity∧middleFour⇒comm instead."
    #-}
    comm+cancelˡ⇒cancelʳ = comm∧cancelˡ⇒cancelʳ
    {-# WARNING_ON_USAGE comm+cancelˡ⇒cancelʳ
    "Warning: comm+cancelˡ⇒cancelʳ was deprecated in v2.0.
    Please use comm∧cancelˡ⇒cancelʳ instead."
    #-}
    comm+cancelʳ⇒cancelˡ = comm∧cancelʳ⇒cancelˡ
    {-# WARNING_ON_USAGE comm+cancelʳ⇒cancelˡ
    "Warning: comm+cancelʳ⇒cancelˡ was deprecated in v2.0.
    Please use comm∧cancelʳ⇒cancelˡ instead."
    #-}
    comm+idˡ⇒idʳ = comm∧idˡ⇒idʳ
    {-# WARNING_ON_USAGE comm+idˡ⇒idʳ
    "Warning: comm+idˡ⇒idʳ was deprecated in v2.0.
    Please use comm∧idˡ⇒idʳ instead."
    #-}
    comm+idʳ⇒idˡ = comm∧idʳ⇒idˡ
    {-# WARNING_ON_USAGE comm+idʳ⇒idˡ
    "Warning: comm+idʳ⇒idˡ was deprecated in v2.0.
    Please use comm∧idʳ⇒idˡ instead."
    #-}
    comm+zeˡ⇒zeʳ = comm∧zeˡ⇒zeʳ
    {-# WARNING_ON_USAGE comm+zeˡ⇒zeʳ
    "Warning: comm+zeˡ⇒zeʳ was deprecated in v2.0.
    Please use comm∧zeˡ⇒zeʳ instead."
    #-}
    comm+zeʳ⇒zeˡ = comm∧zeʳ⇒zeˡ
    {-# WARNING_ON_USAGE comm+zeʳ⇒zeˡ
    "Warning: comm+zeʳ⇒zeˡ was deprecated in v2.0.
    Please use comm∧zeʳ⇒zeˡ instead."
    #-}
    comm+almostCancelˡ⇒almostCancelʳ = comm∧almostCancelˡ⇒almostCancelʳ
    {-# WARNING_ON_USAGE comm+almostCancelˡ⇒almostCancelʳ
    "Warning: comm+almostCancelˡ⇒almostCancelʳ was deprecated in v2.0.
    Please use comm∧almostCancelˡ⇒almostCancelʳ instead."
    #-}
    comm+almostCancelʳ⇒almostCancelˡ = comm∧almostCancelʳ⇒almostCancelˡ
    {-# WARNING_ON_USAGE comm+almostCancelʳ⇒almostCancelˡ
    "Warning: comm+almostCancelʳ⇒almostCancelˡ was deprecated in v2.0.
    Please use comm∧almostCancelʳ⇒almostCancelˡ instead."
    #-}
    comm+invˡ⇒invʳ = comm∧invˡ⇒invʳ
    {-# WARNING_ON_USAGE comm+invˡ⇒invʳ
    "Warning: comm+invˡ⇒invʳ was deprecated in v2.0.
    Please use comm∧invˡ⇒invʳ instead."
    #-}
    comm+invʳ⇒invˡ = comm∧invʳ⇒invˡ
    {-# WARNING_ON_USAGE comm+invʳ⇒invˡ
    "Warning: comm+invʳ⇒invˡ was deprecated in v2.0.
    Please use comm∧invʳ⇒invˡ instead."
    #-}
    comm+invˡ⇒inv = comm∧invˡ⇒inv
    {-# WARNING_ON_USAGE comm+invˡ⇒inv
    "Warning: comm+invˡ⇒inv was deprecated in v2.0.
    Please use comm∧invˡ⇒inv instead."
    #-}
    comm+invʳ⇒inv = comm∧invʳ⇒inv
    {-# WARNING_ON_USAGE comm+invʳ⇒inv
    "Warning: comm+invʳ⇒inv was deprecated in v2.0.
    Please use comm∧invʳ⇒inv instead."
    #-}
    comm+distrˡ⇒distrʳ = comm∧distrˡ⇒distrʳ
    {-# WARNING_ON_USAGE comm+distrˡ⇒distrʳ
    "Warning: comm+distrˡ⇒distrʳ was deprecated in v2.0.
    Please use comm∧distrˡ⇒distrʳ instead."
    #-}
    comm+distrʳ⇒distrˡ = comm∧distrʳ⇒distrˡ
    {-# WARNING_ON_USAGE comm+distrʳ⇒distrˡ
    "Warning: comm+distrʳ⇒distrˡ was deprecated in v2.0.
    Please use comm∧distrʳ⇒distrˡ instead."
    #-}
    assoc+distribʳ+idʳ+invʳ⇒zeˡ = assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ
    {-# WARNING_ON_USAGE assoc+distribʳ+idʳ+invʳ⇒zeˡ
    "Warning: assoc+distribʳ+idʳ+invʳ⇒zeˡ was deprecated in v2.0.
    Please use assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ instead."
    #-}
    assoc+distribˡ+idʳ+invʳ⇒zeʳ = assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ
    {-# WARNING_ON_USAGE assoc+distribˡ+idʳ+invʳ⇒zeʳ
    "Warning: assoc+distribˡ+idʳ+invʳ⇒zeʳ was deprecated in v2.0.
    Please use assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ instead."
    #-}
    assoc+id+invʳ⇒invˡ-unique = assoc∧id∧invʳ⇒invˡ-unique
    {-# WARNING_ON_USAGE assoc+id+invʳ⇒invˡ-unique
    "Warning: assoc+id+invʳ⇒invˡ-unique was deprecated in v2.0.
    Please use assoc∧id∧invʳ⇒invˡ-unique instead."
    #-}
    assoc+id+invˡ⇒invʳ-unique = assoc∧id∧invˡ⇒invʳ-unique
    {-# WARNING_ON_USAGE assoc+id+invˡ⇒invʳ-unique
    "Warning: assoc+id+invˡ⇒invʳ-unique was deprecated in v2.0.
    Please use assoc∧id∧invˡ⇒invʳ-unique instead."
    #-}
    subst+comm⇒sym = subst∧comm⇒sym
    {-# WARNING_ON_USAGE subst+comm⇒sym
    "Warning: subst+comm⇒sym was deprecated in v2.0.
    Please use subst∧comm⇒sym instead."
    #-}