    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Relations between properties of functions, such as associativity and
    -- commutativity (specialised to propositional equality)
    ------------------------------------------------------------------------

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

    module Algebra.Consequences.Propositional
      {a} {A : Set a} where

    open import Algebra.Core using (Op₁; Op₂)
    open import Data.Sum.Base using (inj₁; inj₂)
    open import Relation.Binary.Core using (Rel)
    open import Relation.Binary.Bundles using (Setoid)
    open import Relation.Binary.Definitions using (Symmetric; Total)
    open import Relation.Binary.PropositionalEquality.Core
      using (_≡_; cong₂; subst)
    open import Relation.Binary.PropositionalEquality.Properties
      using (setoid)
    open import Relation.Unary using (Pred)

    open import Algebra.Definitions {A = A} _≡_
    import Algebra.Consequences.Setoid (setoid A) as Base

    ------------------------------------------------------------------------
    -- Re-export all proofs that don't require congruence or substitutivity

    open Base public
      hiding
      ( comm∧assoc⇒middleFour
      ; identity∧middleFour⇒assoc
      ; identity∧middleFour⇒comm
      ; assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ
      ; assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ
      ; assoc∧id∧invʳ⇒invˡ-unique
      ; assoc∧id∧invˡ⇒invʳ-unique
      ; comm∧distrˡ⇒distrʳ
      ; comm∧distrʳ⇒distrˡ
      ; comm⇒sym[distribˡ]
      ; subst∧comm⇒sym
      ; wlog
      ; sel⇒idem
    -- plus all the deprecated versions of the above
      ; comm+assoc⇒middleFour
      ; identity+middleFour⇒assoc
      ; identity+middleFour⇒comm
      ; assoc+distribʳ+idʳ+invʳ⇒zeˡ
      ; assoc+distribˡ+idʳ+invʳ⇒zeʳ
      ; assoc+id+invʳ⇒invˡ-unique
      ; assoc+id+invˡ⇒invʳ-unique
      ; comm+distrˡ⇒distrʳ
      ; comm+distrʳ⇒distrˡ
      ; subst+comm⇒sym
      )

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

    module _ {_∙_ _⁻¹ ε} where

      assoc∧id∧invʳ⇒invˡ-unique : Associative _∙_ → Identity ε _∙_ →
                                  RightInverse ε _⁻¹ _∙_ →
                                  ∀ x y → (x ∙ y) ≡ ε → x ≡ (y ⁻¹)
      assoc∧id∧invʳ⇒invˡ-unique = Base.assoc∧id∧invʳ⇒invˡ-unique (cong₂ _)

      assoc∧id∧invˡ⇒invʳ-unique : Associative _∙_ → Identity ε _∙_ →
                                  LeftInverse ε _⁻¹ _∙_ →
                                  ∀ x y → (x ∙ y) ≡ ε → y ≡ (x ⁻¹)
      assoc∧id∧invˡ⇒invʳ-unique = Base.assoc∧id∧invˡ⇒invʳ-unique (cong₂ _)

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

    module _ {_+_ _*_ -_ 0#} where

      assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ : Associative _+_ → _*_ DistributesOverʳ _+_ →
                                    RightIdentity 0# _+_ → RightInverse 0# -_ _+_ →
                                    LeftZero 0# _*_
      assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ =
        Base.assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ (cong₂ _+_) (cong₂ _*_)

      assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ : Associative _+_ → _*_ DistributesOverˡ _+_ →
                                    RightIdentity 0# _+_ → RightInverse 0# -_ _+_ →
                                    RightZero 0# _*_
      assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ =
        Base.assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ (cong₂ _+_) (cong₂ _*_)

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

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

      comm∧distrˡ⇒distrʳ : _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOverʳ _◦_
      comm∧distrˡ⇒distrʳ = Base.comm+distrˡ⇒distrʳ (cong₂ _) ∙-comm

      comm∧distrʳ⇒distrˡ : _∙_ DistributesOverʳ _◦_ → _∙_ DistributesOverˡ _◦_
      comm∧distrʳ⇒distrˡ = Base.comm∧distrʳ⇒distrˡ (cong₂ _) ∙-comm

      comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y ∙ z)) ≡ ((x ◦ y) ∙ (x ◦ z)))
      comm⇒sym[distribˡ] = Base.comm⇒sym[distribˡ] (cong₂ _◦_) ∙-comm

    ------------------------------------------------------------------------
    -- Selectivity

    module _ {_∙_ : Op₂ A} where

      sel⇒idem : Selective _∙_ → Idempotent _∙_
      sel⇒idem = Base.sel⇒idem _≡_

    ------------------------------------------------------------------------
    -- Middle-Four Exchange

    module _ {_∙_ : Op₂ A} where

      comm∧assoc⇒middleFour : Commutative _∙_ → Associative _∙_ →
                              _∙_ MiddleFourExchange _∙_
      comm∧assoc⇒middleFour = Base.comm∧assoc⇒middleFour (cong₂ _∙_)

      identity∧middleFour⇒assoc : {e : A} → Identity e _∙_ →
                                  _∙_ MiddleFourExchange _∙_ →
                                  Associative _∙_
      identity∧middleFour⇒assoc = Base.identity∧middleFour⇒assoc (cong₂ _∙_)

      identity∧middleFour⇒comm : {_+_ : Op₂ A} {e : A} → Identity e _+_ →
                                 _∙_ MiddleFourExchange _+_ →
                                 Commutative _∙_
      identity∧middleFour⇒comm = Base.identity∧middleFour⇒comm (cong₂ _∙_)

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

    module _ {p} {P : Pred A p} where

      subst∧comm⇒sym : ∀ {f} (f-comm : Commutative f) →
                       Symmetric (λ a b → P (f a b))
      subst∧comm⇒sym = Base.subst∧comm⇒sym {P = P} subst

      wlog : ∀ {f} (f-comm : Commutative f) →
             ∀ {r} {_R_ : Rel _ r} → Total _R_ →
             (∀ a b → a R b → P (f a b)) →
             ∀ a b → P (f a b)
      wlog = Base.wlog {P = P} subst

    ------------------------------------------------------------------------
    -- 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+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."
    #-}