    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Some algebraic structures (not packed up with sets, operations, etc.)
    ------------------------------------------------------------------------

    -- The contents of this module should be accessed via `Algebra`, unless
    -- you want to parameterise it via the equality relation.

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

    open import Relation.Binary.Core using (Rel)
    open import Relation.Binary.Bundles using (Setoid)
    open import Relation.Binary.Structures using (IsEquivalence)

    module Algebra.Structures
      {a ℓ} {A : Set a}  -- The underlying set
      (_≈_ : Rel A ℓ)    -- The underlying equality relation
      where

    -- The file is divided into sections depending on the arities of the
    -- components of the algebraic structure.

    open import Algebra.Core using (Op₁; Op₂)
    open import Algebra.Definitions _≈_
    import Algebra.Consequences.Setoid as Consequences
    open import Data.Product.Base using (_,_; proj₁; proj₂)
    open import Level using (_⊔_)

    ------------------------------------------------------------------------
    -- Structures with 1 unary operation & 1 element
    ------------------------------------------------------------------------

    record IsSuccessorSet (suc# : Op₁ A) (zero# : A) : Set (a ⊔ ℓ) where
      field
        isEquivalence : IsEquivalence _≈_
        suc#-cong     : Congruent₁ suc#

      open IsEquivalence isEquivalence public

      setoid : Setoid a ℓ
      setoid = record { isEquivalence = isEquivalence }

    ------------------------------------------------------------------------
    -- Structures with 1 binary operation
    ------------------------------------------------------------------------

    record IsMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
      field
        isEquivalence : IsEquivalence _≈_
        ∙-cong        : Congruent₂ ∙

      open IsEquivalence isEquivalence public

      setoid : Setoid a ℓ
      setoid = record { isEquivalence = isEquivalence }

      open Consequences.Congruence setoid ∙-cong public

    record IsCommutativeMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
      field
        isMagma : IsMagma ∙
        comm    : Commutative ∙

      open IsMagma isMagma public

    record IsIdempotentMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
      field
        isMagma : IsMagma ∙
        idem    : Idempotent ∙

      open IsMagma isMagma public

    record IsAlternativeMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
      field
        isMagma  : IsMagma ∙
        alter    : Alternative ∙

      open IsMagma isMagma public

      alternativeˡ : LeftAlternative ∙
      alternativeˡ = proj₁ alter

      alternativeʳ : RightAlternative ∙
      alternativeʳ = proj₂ alter

    record IsFlexibleMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
      field
        isMagma  : IsMagma ∙
        flex     : Flexible ∙

      open IsMagma isMagma public

    record IsMedialMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
      field
        isMagma : IsMagma ∙
        medial  : Medial ∙

      open IsMagma isMagma public

    record IsSemimedialMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
      field
        isMagma    : IsMagma ∙
        semiMedial : Semimedial ∙

      open IsMagma isMagma public

      semimedialˡ : LeftSemimedial ∙
      semimedialˡ = proj₁ semiMedial

      semimedialʳ : RightSemimedial ∙
      semimedialʳ = proj₂ semiMedial

    record IsSelectiveMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
      field
        isMagma : IsMagma ∙
        sel     : Selective ∙

      open IsMagma isMagma public

    record IsSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ) where
      field
        isMagma : IsMagma ∙
        assoc   : Associative ∙

      open IsMagma isMagma public

    record IsBand (∙ : Op₂ A) : Set (a ⊔ ℓ) where
      field
        isSemigroup : IsSemigroup ∙
        idem        : Idempotent ∙

      open IsSemigroup isSemigroup public

    record IsCommutativeSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ) where
      field
        isSemigroup : IsSemigroup ∙
        comm        : Commutative ∙

      open IsSemigroup isSemigroup public

      isCommutativeMagma : IsCommutativeMagma ∙
      isCommutativeMagma = record
        { isMagma = isMagma
        ; comm    = comm
        }

    record IsCommutativeBand (∙ : Op₂ A) : Set (a ⊔ ℓ) where
      field
        isBand : IsBand ∙
        comm   : Commutative ∙

      open IsBand isBand public

      isCommutativeSemigroup : IsCommutativeSemigroup ∙
      isCommutativeSemigroup = record { isSemigroup = isSemigroup ; comm = comm }

      open IsCommutativeSemigroup isCommutativeSemigroup public
        using (isCommutativeMagma)

    ------------------------------------------------------------------------
    -- Structures with 1 binary operation & 1 element
    ------------------------------------------------------------------------

    record IsUnitalMagma (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
      field
        isMagma  : IsMagma ∙
        identity : Identity ε ∙

      open IsMagma isMagma public

      identityˡ : LeftIdentity ε ∙
      identityˡ = proj₁ identity

      identityʳ : RightIdentity ε ∙
      identityʳ = proj₂ identity

    record IsMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
      field
        isSemigroup : IsSemigroup ∙
        identity    : Identity ε ∙

      open IsSemigroup isSemigroup public

      identityˡ : LeftIdentity ε ∙
      identityˡ = proj₁ identity

      identityʳ : RightIdentity ε ∙
      identityʳ = proj₂ identity

      isUnitalMagma : IsUnitalMagma ∙ ε
      isUnitalMagma = record
        { isMagma  = isMagma
        ; identity = identity
        }

    record IsCommutativeMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
      field
        isMonoid : IsMonoid ∙ ε
        comm     : Commutative ∙

      open IsMonoid isMonoid public

      isCommutativeSemigroup : IsCommutativeSemigroup ∙
      isCommutativeSemigroup = record
        { isSemigroup = isSemigroup
        ; comm        = comm
        }

      open IsCommutativeSemigroup isCommutativeSemigroup public
        using (isCommutativeMagma)

    record IsIdempotentMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
      field
        isMonoid : IsMonoid ∙ ε
        idem     : Idempotent ∙

      open IsMonoid isMonoid public

      isBand : IsBand ∙
      isBand = record { isSemigroup = isSemigroup ; idem = idem }

    record IsIdempotentCommutativeMonoid (∙ : Op₂ A)
                                         (ε : A) : Set (a ⊔ ℓ) where
      field
        isCommutativeMonoid : IsCommutativeMonoid ∙ ε
        idem                : Idempotent ∙

      open IsCommutativeMonoid isCommutativeMonoid public

      isIdempotentMonoid : IsIdempotentMonoid ∙ ε
      isIdempotentMonoid = record { isMonoid = isMonoid ; idem = idem }

      open IsIdempotentMonoid isIdempotentMonoid public
        using (isBand)

      isCommutativeBand : IsCommutativeBand ∙
      isCommutativeBand = record { isBand = isBand ; comm = comm }

    ------------------------------------------------------------------------
    -- Structures with 1 binary operation, 1 unary operation & 1 element
    ------------------------------------------------------------------------

    record IsInvertibleMagma (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where
      field
        isMagma  : IsMagma _∙_
        inverse   : Inverse ε _⁻¹ _∙_
        ⁻¹-cong   : Congruent₁ _⁻¹

      open IsMagma isMagma public

      inverseˡ : LeftInverse ε _⁻¹ _∙_
      inverseˡ = proj₁ inverse

      inverseʳ : RightInverse ε _⁻¹ _∙_
      inverseʳ = proj₂ inverse

    record IsInvertibleUnitalMagma (_∙_ : Op₂ A) (ε : A) (⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where
      field
        isInvertibleMagma : IsInvertibleMagma _∙_  ε ⁻¹
        identity          : Identity ε _∙_

      open IsInvertibleMagma isInvertibleMagma public

      identityˡ : LeftIdentity ε _∙_
      identityˡ = proj₁ identity

      identityʳ : RightIdentity ε _∙_
      identityʳ = proj₂ identity

      isUnitalMagma : IsUnitalMagma _∙_  ε
      isUnitalMagma = record
        { isMagma  = isMagma
        ; identity = identity
        }

    record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where
      field
        isMonoid  : IsMonoid _∙_ ε
        inverse   : Inverse ε _⁻¹ _∙_
        ⁻¹-cong   : Congruent₁ _⁻¹

      open IsMonoid isMonoid public

      infixr 6 _\\_
      _\\_ : Op₂ A
      x \\ y = (x ⁻¹) ∙ y

      infixl 6 _//_
      _//_ : Op₂ A
      x // y = x ∙ (y ⁻¹)

      -- Deprecated.
      infixl 6 _-_
      _-_ : Op₂ A
      _-_ = _//_
      {-# WARNING_ON_USAGE _-_
      "Warning: _-_ was deprecated in v2.1.
      Please use _//_ instead. "
      #-}

      inverseˡ : LeftInverse ε _⁻¹ _∙_
      inverseˡ = proj₁ inverse

      inverseʳ : RightInverse ε _⁻¹ _∙_
      inverseʳ = proj₂ inverse

      uniqueˡ-⁻¹ : ∀ x y → (x ∙ y) ≈ ε → x ≈ (y ⁻¹)
      uniqueˡ-⁻¹ = Consequences.assoc∧id∧invʳ⇒invˡ-unique
                    setoid ∙-cong assoc identity inverseʳ
      {-# WARNING_ON_USAGE uniqueˡ-⁻¹
      "Warning: uniqueˡ-⁻¹ was deprecated in v2.3.
      Please use Algebra.Properties.Group.inverseˡ-unique instead. "
      #-}

      uniqueʳ-⁻¹ : ∀ x y → (x ∙ y) ≈ ε → y ≈ (x ⁻¹)
      uniqueʳ-⁻¹ = Consequences.assoc∧id∧invˡ⇒invʳ-unique
                    setoid ∙-cong assoc identity inverseˡ
      {-# WARNING_ON_USAGE uniqueʳ-⁻¹
      "Warning: uniqueʳ-⁻¹ was deprecated in v2.3.
      Please use Algebra.Properties.Group.inverseʳ-unique instead. "
      #-}

      isInvertibleMagma : IsInvertibleMagma _∙_ ε _⁻¹
      isInvertibleMagma = record
        { isMagma = isMagma
        ; inverse = inverse
        ; ⁻¹-cong = ⁻¹-cong
        }

      isInvertibleUnitalMagma : IsInvertibleUnitalMagma _∙_ ε _⁻¹
      isInvertibleUnitalMagma = record
        { isInvertibleMagma = isInvertibleMagma
        ; identity = identity
        }

    record IsAbelianGroup (∙ : Op₂ A)
                          (ε : A) (⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where
      field
        isGroup : IsGroup ∙ ε ⁻¹
        comm    : Commutative ∙

      open IsGroup isGroup public renaming (_//_ to _-_) hiding (_\\_; _-_)

      isCommutativeMonoid : IsCommutativeMonoid ∙ ε
      isCommutativeMonoid = record
        { isMonoid = isMonoid
        ; comm     = comm
        }

      open IsCommutativeMonoid isCommutativeMonoid public
        using (isCommutativeMagma; isCommutativeSemigroup)

    ------------------------------------------------------------------------
    -- Structures with 2 binary operations & 1 element
    ------------------------------------------------------------------------

    record IsNearSemiring (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
      field
        +-isMonoid    : IsMonoid + 0#
        *-cong        : Congruent₂ *
        *-assoc       : Associative *
        distribʳ      : * DistributesOverʳ +
        zeroˡ         : LeftZero 0# *

      open IsMonoid +-isMonoid public
        renaming
        ( assoc         to +-assoc
        ; ∙-cong        to +-cong
        ; ∙-congˡ       to +-congˡ
        ; ∙-congʳ       to +-congʳ
        ; identity      to +-identity
        ; identityˡ     to +-identityˡ
        ; identityʳ     to +-identityʳ
        ; isMagma       to +-isMagma
        ; isUnitalMagma to +-isUnitalMagma
        ; isSemigroup   to +-isSemigroup
        )

      *-isMagma : IsMagma *
      *-isMagma = record
        { isEquivalence = isEquivalence
        ; ∙-cong        = *-cong
        }

      *-isSemigroup : IsSemigroup *
      *-isSemigroup = record
        { isMagma = *-isMagma
        ; assoc   = *-assoc
        }

      open IsMagma *-isMagma public
        using ()
        renaming
        ( ∙-congˡ  to *-congˡ
        ; ∙-congʳ  to *-congʳ
        )

    record IsSemiringWithoutOne (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
      field
        +-isCommutativeMonoid : IsCommutativeMonoid + 0#
        *-cong                : Congruent₂ *
        *-assoc               : Associative *
        distrib               : * DistributesOver +
        zero                  : Zero 0# *

      open IsCommutativeMonoid +-isCommutativeMonoid public
        using (setoid; isEquivalence)
        renaming
        ( ∙-cong                 to +-cong
        ; ∙-congˡ                to +-congˡ
        ; ∙-congʳ                to +-congʳ
        ; assoc                  to +-assoc
        ; identity               to +-identity
        ; identityˡ              to +-identityˡ
        ; identityʳ              to +-identityʳ
        ; comm                   to +-comm
        ; isMonoid               to +-isMonoid
        ; isCommutativeMagma     to +-isCommutativeMagma
        ; isCommutativeSemigroup to +-isCommutativeSemigroup
        )

      open IsEquivalence isEquivalence public

      *-isMagma : IsMagma *
      *-isMagma = record
        { isEquivalence = isEquivalence
        ; ∙-cong        = *-cong
        }

      *-isSemigroup : IsSemigroup *
      *-isSemigroup = record
        { isMagma = *-isMagma
        ; assoc   = *-assoc
        }

      open IsMagma *-isMagma public
        using ()
        renaming
        ( ∙-congˡ to *-congˡ
        ; ∙-congʳ to *-congʳ
        )

      distribˡ : * DistributesOverˡ +
      distribˡ = proj₁ distrib

      distribʳ : * DistributesOverʳ +
      distribʳ = proj₂ distrib

      zeroˡ : LeftZero 0# *
      zeroˡ = proj₁ zero

      zeroʳ : RightZero 0# *
      zeroʳ = proj₂ zero

      isNearSemiring : IsNearSemiring + * 0#
      isNearSemiring = record
        { +-isMonoid    = +-isMonoid
        ; *-cong        = *-cong
        ; *-assoc       = *-assoc
        ; distribʳ      = proj₂ distrib
        ; zeroˡ         = zeroˡ
        }

    record IsCommutativeSemiringWithoutOne
             (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
      field
        isSemiringWithoutOne : IsSemiringWithoutOne + * 0#
        *-comm               : Commutative *

      open IsSemiringWithoutOne isSemiringWithoutOne public

      *-isCommutativeSemigroup : IsCommutativeSemigroup *
      *-isCommutativeSemigroup = record
        { isSemigroup = *-isSemigroup
        ; comm        = *-comm
        }

      open IsCommutativeSemigroup *-isCommutativeSemigroup public
        using () renaming (isCommutativeMagma to *-isCommutativeMagma)

    ------------------------------------------------------------------------
    -- Structures with 2 binary operations & 2 elements
    ------------------------------------------------------------------------

    record IsSemiringWithoutAnnihilatingZero (+ * : Op₂ A)
                                             (0# 1# : A) : Set (a ⊔ ℓ) where
      field
        -- Note that these structures do have an additive unit, but this
        -- unit does not necessarily annihilate multiplication.
        +-isCommutativeMonoid : IsCommutativeMonoid + 0#
        *-cong                : Congruent₂ *
        *-assoc               : Associative *
        *-identity            : Identity 1# *
        distrib               : * DistributesOver +

      distribˡ : * DistributesOverˡ +
      distribˡ = proj₁ distrib

      distribʳ : * DistributesOverʳ +
      distribʳ = proj₂ distrib

      open IsCommutativeMonoid +-isCommutativeMonoid public
        renaming
        ( assoc                  to +-assoc
        ; ∙-cong                 to +-cong
        ; ∙-congˡ                to +-congˡ
        ; ∙-congʳ                to +-congʳ
        ; identity               to +-identity
        ; identityˡ              to +-identityˡ
        ; identityʳ              to +-identityʳ
        ; comm                   to +-comm
        ; isMagma                to +-isMagma
        ; isSemigroup            to +-isSemigroup
        ; isMonoid               to +-isMonoid
        ; isUnitalMagma          to +-isUnitalMagma
        ; isCommutativeMagma     to +-isCommutativeMagma
        ; isCommutativeSemigroup to +-isCommutativeSemigroup
        )

      *-isMagma : IsMagma *
      *-isMagma = record
        { isEquivalence = isEquivalence
        ; ∙-cong        = *-cong
        }

      *-isSemigroup : IsSemigroup *
      *-isSemigroup = record
        { isMagma = *-isMagma
        ; assoc   = *-assoc
        }

      *-isMonoid : IsMonoid * 1#
      *-isMonoid = record
        { isSemigroup = *-isSemigroup
        ; identity    = *-identity
        }

      open IsMonoid *-isMonoid public
        using ()
        renaming
        ( ∙-congˡ     to *-congˡ
        ; ∙-congʳ     to *-congʳ
        ; identityˡ   to *-identityˡ
        ; identityʳ   to *-identityʳ
        )

    record IsSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
      field
        isSemiringWithoutAnnihilatingZero :
          IsSemiringWithoutAnnihilatingZero + * 0# 1#
        zero : Zero 0# *

      open IsSemiringWithoutAnnihilatingZero
             isSemiringWithoutAnnihilatingZero public

      isSemiringWithoutOne : IsSemiringWithoutOne + * 0#
      isSemiringWithoutOne = record
        { +-isCommutativeMonoid = +-isCommutativeMonoid
        ; *-cong                = *-cong
        ; *-assoc               = *-assoc
        ; distrib               = distrib
        ; zero                  = zero
        }

      open IsSemiringWithoutOne isSemiringWithoutOne public
        using
        ( isNearSemiring
        ; zeroˡ
        ; zeroʳ
        )

    record IsCommutativeSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
      field
        isSemiring : IsSemiring + * 0# 1#
        *-comm     : Commutative *

      open IsSemiring isSemiring public

      isCommutativeSemiringWithoutOne :
        IsCommutativeSemiringWithoutOne + * 0#
      isCommutativeSemiringWithoutOne = record
        { isSemiringWithoutOne = isSemiringWithoutOne
        ; *-comm = *-comm
        }

      open IsCommutativeSemiringWithoutOne isCommutativeSemiringWithoutOne public
        using
        ( *-isCommutativeMagma
        ; *-isCommutativeSemigroup
        )

      *-isCommutativeMonoid : IsCommutativeMonoid * 1#
      *-isCommutativeMonoid = record
        { isMonoid = *-isMonoid
        ; comm     = *-comm
        }

    record IsCancellativeCommutativeSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
      field
        isCommutativeSemiring : IsCommutativeSemiring + * 0# 1#
        *-cancelˡ-nonZero     : AlmostLeftCancellative 0# *

      open IsCommutativeSemiring isCommutativeSemiring public

      *-cancelʳ-nonZero : AlmostRightCancellative 0# *
      *-cancelʳ-nonZero = Consequences.comm∧almostCancelˡ⇒almostCancelʳ setoid
          *-comm *-cancelˡ-nonZero

    record IsIdempotentSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
      field
        isSemiring     : IsSemiring + * 0# 1#
        +-idem         : Idempotent +

      open IsSemiring isSemiring public

      +-isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid + 0#
      +-isIdempotentCommutativeMonoid = record
        { isCommutativeMonoid = +-isCommutativeMonoid
        ; idem = +-idem
        }

      open IsIdempotentCommutativeMonoid +-isIdempotentCommutativeMonoid public
        using ()
        renaming ( isCommutativeBand to +-isCommutativeBand
                 ; isBand to +-isBand
                 ; isIdempotentMonoid to +-isIdempotentMonoid
                 )

    record IsKleeneAlgebra (+ * : Op₂ A) (⋆ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
      field
        isIdempotentSemiring  : IsIdempotentSemiring + * 0# 1#
        starExpansive         : StarExpansive 1# + * ⋆
        starDestructive       : StarDestructive + * ⋆

      open IsIdempotentSemiring isIdempotentSemiring public

      starExpansiveˡ : StarLeftExpansive 1# + * ⋆
      starExpansiveˡ = proj₁ starExpansive

      starExpansiveʳ : StarRightExpansive 1# + * ⋆
      starExpansiveʳ = proj₂ starExpansive

      starDestructiveˡ : StarLeftDestructive + * ⋆
      starDestructiveˡ = proj₁ starDestructive

      starDestructiveʳ : StarRightDestructive + * ⋆
      starDestructiveʳ = proj₂ starDestructive

    record IsQuasiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
      field
        +-isMonoid    : IsMonoid + 0#
        *-cong        : Congruent₂ *
        *-assoc       : Associative *
        *-identity    : Identity 1# *
        distrib       : * DistributesOver +
        zero          : Zero 0# *

      open IsMonoid +-isMonoid public
        renaming
        ( assoc         to +-assoc
        ; ∙-cong        to +-cong
        ; ∙-congˡ       to +-congˡ
        ; ∙-congʳ       to +-congʳ
        ; identity      to +-identity
        ; identityˡ     to +-identityˡ
        ; identityʳ     to +-identityʳ
        ; isMagma       to +-isMagma
        ; isUnitalMagma to +-isUnitalMagma
        ; isSemigroup   to +-isSemigroup
        )

      distribˡ : * DistributesOverˡ +
      distribˡ = proj₁ distrib

      distribʳ : * DistributesOverʳ +
      distribʳ = proj₂ distrib

      zeroˡ : LeftZero 0# *
      zeroˡ = proj₁ zero

      zeroʳ : RightZero 0# *
      zeroʳ = proj₂ zero

      identityˡ : LeftIdentity 1# *
      identityˡ = proj₁ *-identity

      identityʳ : RightIdentity 1# *
      identityʳ = proj₂ *-identity

      *-isMagma : IsMagma *
      *-isMagma = record
        { isEquivalence = isEquivalence
        ; ∙-cong        = *-cong
        }

      *-isSemigroup : IsSemigroup *
      *-isSemigroup = record
        { isMagma = *-isMagma
        ; assoc   = *-assoc
        }

      *-isMonoid : IsMonoid * 1#
      *-isMonoid = record
        { isSemigroup = *-isSemigroup
        ; identity    = *-identity
        }

      open IsMonoid *-isMonoid public
        using ()
        renaming
        ( ∙-congˡ     to *-congˡ
        ; ∙-congʳ     to *-congʳ
        ; identityˡ   to *-identityˡ
        ; identityʳ   to *-identityʳ
        )

    ------------------------------------------------------------------------
    -- Structures with 2 binary operations, 1 unary operation & 1 element
    ------------------------------------------------------------------------

    record IsRingWithoutOne (+ * : Op₂ A) (-_ : Op₁ A) (0# : A) : Set (a ⊔ ℓ) where
      field
        +-isAbelianGroup : IsAbelianGroup + 0# -_
        *-cong           : Congruent₂ *
        *-assoc          : Associative *
        distrib          : * DistributesOver +

      open IsAbelianGroup +-isAbelianGroup public
        renaming
        ( assoc                   to +-assoc
        ; ∙-cong                  to +-cong
        ; ∙-congˡ                 to +-congˡ
        ; ∙-congʳ                 to +-congʳ
        ; identity                to +-identity
        ; identityˡ               to +-identityˡ
        ; identityʳ               to +-identityʳ
        ; inverse                 to -‿inverse
        ; inverseˡ                to -‿inverseˡ
        ; inverseʳ                to -‿inverseʳ
        ; ⁻¹-cong                 to -‿cong
        ; comm                    to +-comm
        ; isMagma                 to +-isMagma
        ; isSemigroup             to +-isSemigroup
        ; isMonoid                to +-isMonoid
        ; isUnitalMagma           to +-isUnitalMagma
        ; isCommutativeMagma      to +-isCommutativeMagma
        ; isCommutativeMonoid     to +-isCommutativeMonoid
        ; isCommutativeSemigroup  to +-isCommutativeSemigroup
        ; isInvertibleMagma       to +-isInvertibleMagma
        ; isInvertibleUnitalMagma to +-isInvertibleUnitalMagma
        ; isGroup                 to +-isGroup
        )

      distribˡ : * DistributesOverˡ +
      distribˡ = proj₁ distrib

      distribʳ : * DistributesOverʳ +
      distribʳ = proj₂ distrib

      zeroˡ : LeftZero 0# *
      zeroˡ = Consequences.assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ setoid
        +-cong *-cong +-assoc distribʳ +-identityʳ -‿inverseʳ

      zeroʳ : RightZero 0# *
      zeroʳ = Consequences.assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ setoid
        +-cong *-cong +-assoc distribˡ +-identityʳ -‿inverseʳ

      zero : Zero 0# *
      zero = zeroˡ , zeroʳ

      isNearSemiring : IsNearSemiring + * 0#
      isNearSemiring = record
        { +-isMonoid = +-isMonoid
        ; *-cong = *-cong
        ; *-assoc = *-assoc
        ; distribʳ = distribʳ
        ; zeroˡ = zeroˡ
        }

      open IsNearSemiring isNearSemiring public
        using (*-isMagma; *-isSemigroup; *-congˡ; *-congʳ)

    ------------------------------------------------------------------------
    -- Structures with 2 binary operations, 1 unary operation & 2 elements
    ------------------------------------------------------------------------

    record IsNonAssociativeRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
      field
        +-isAbelianGroup : IsAbelianGroup + 0# -_
        *-cong           : Congruent₂ *
        *-identity       : Identity 1# *
        distrib          : * DistributesOver +
        zero             : Zero 0# *

      open IsAbelianGroup +-isAbelianGroup public
        renaming
        ( assoc                   to +-assoc
        ; ∙-cong                  to +-cong
        ; ∙-congˡ                 to +-congˡ
        ; ∙-congʳ                 to +-congʳ
        ; identity                to +-identity
        ; identityˡ               to +-identityˡ
        ; identityʳ               to +-identityʳ
        ; inverse                 to -‿inverse
        ; inverseˡ                to -‿inverseˡ
        ; inverseʳ                to -‿inverseʳ
        ; ⁻¹-cong                 to -‿cong
        ; comm                    to +-comm
        ; isMagma                 to +-isMagma
        ; isSemigroup             to +-isSemigroup
        ; isMonoid                to +-isMonoid
        ; isUnitalMagma           to +-isUnitalMagma
        ; isCommutativeMagma      to +-isCommutativeMagma
        ; isCommutativeMonoid     to +-isCommutativeMonoid
        ; isCommutativeSemigroup  to +-isCommutativeSemigroup
        ; isInvertibleMagma       to +-isInvertibleMagma
        ; isInvertibleUnitalMagma to +-isInvertibleUnitalMagma
        ; isGroup                 to +-isGroup
        )

      zeroˡ : LeftZero 0# *
      zeroˡ = proj₁ zero

      zeroʳ : RightZero 0# *
      zeroʳ = proj₂ zero

      distribˡ : * DistributesOverˡ +
      distribˡ = proj₁ distrib

      distribʳ : * DistributesOverʳ +
      distribʳ = proj₂ distrib

      *-isMagma : IsMagma *
      *-isMagma = record
        { isEquivalence = isEquivalence
        ; ∙-cong        = *-cong
        }

      *-identityˡ : LeftIdentity 1# *
      *-identityˡ = proj₁ *-identity

      *-identityʳ : RightIdentity 1# *
      *-identityʳ = proj₂ *-identity

      *-isUnitalMagma : IsUnitalMagma * 1#
      *-isUnitalMagma = record
        { isMagma = *-isMagma
        ; identity = *-identity
        }

      open IsUnitalMagma *-isUnitalMagma public
        using ()
        renaming
        ( ∙-congˡ   to *-congˡ
        ; ∙-congʳ   to *-congʳ
        )

    record IsNearring (+ * : Op₂ A) (0# 1# : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where
      field
        isQuasiring : IsQuasiring + * 0# 1#
        +-inverse   : Inverse 0# _⁻¹ +
        ⁻¹-cong     : Congruent₁ _⁻¹

      open IsQuasiring isQuasiring public

      +-inverseˡ : LeftInverse 0# _⁻¹ +
      +-inverseˡ = proj₁ +-inverse

      +-inverseʳ : RightInverse 0# _⁻¹ +
      +-inverseʳ = proj₂ +-inverse

    record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
      field
        +-isAbelianGroup : IsAbelianGroup + 0# -_
        *-cong           : Congruent₂ *
        *-assoc          : Associative *
        *-identity       : Identity 1# *
        distrib          : * DistributesOver +

      isRingWithoutOne : IsRingWithoutOne + * -_ 0#
      isRingWithoutOne = record
        { +-isAbelianGroup = +-isAbelianGroup
        ; *-cong  = *-cong
        ; *-assoc = *-assoc
        ; distrib = distrib
        }

      open IsRingWithoutOne isRingWithoutOne public
        hiding (+-isAbelianGroup; *-cong; *-assoc; distrib)

      *-isMonoid : IsMonoid * 1#
      *-isMonoid = record
        { isSemigroup = *-isSemigroup
        ; identity    = *-identity
        }

      open IsMonoid *-isMonoid public
        using ()
        renaming
        ( identityˡ   to *-identityˡ
        ; identityʳ   to *-identityʳ
        )

      isSemiringWithoutAnnihilatingZero
        : IsSemiringWithoutAnnihilatingZero + * 0# 1#
      isSemiringWithoutAnnihilatingZero = record
        { +-isCommutativeMonoid = +-isCommutativeMonoid
        ; *-cong                = *-cong
        ; *-assoc               = *-assoc
        ; *-identity            = *-identity
        ; distrib               = distrib
        }

      isSemiring : IsSemiring + * 0# 1#
      isSemiring = record
        { isSemiringWithoutAnnihilatingZero =
            isSemiringWithoutAnnihilatingZero
        ; zero = zero
        }

      open IsSemiring isSemiring public
        using (isSemiringWithoutOne)

    record IsCommutativeRing
             (+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
      field
        isRing : IsRing + * - 0# 1#
        *-comm : Commutative *

      open IsRing isRing public

      isCommutativeSemiring : IsCommutativeSemiring + * 0# 1#
      isCommutativeSemiring = record
        { isSemiring = isSemiring
        ; *-comm = *-comm
        }

      open IsCommutativeSemiring isCommutativeSemiring public
        using
        ( isCommutativeSemiringWithoutOne
        ; *-isCommutativeMagma
        ; *-isCommutativeSemigroup
        ; *-isCommutativeMonoid
        )

    ------------------------------------------------------------------------
    -- Structures with 3 binary operations
    ------------------------------------------------------------------------

    record IsQuasigroup (∙ \\ // : Op₂ A) : Set (a ⊔ ℓ) where
      field
        isMagma       : IsMagma ∙
        \\-cong       : Congruent₂ \\
        //-cong       : Congruent₂ //
        leftDivides   : LeftDivides ∙ \\
        rightDivides  : RightDivides ∙ //

      open IsMagma isMagma public

      \\-congˡ : LeftCongruent \\
      \\-congˡ y≈z = \\-cong refl y≈z

      \\-congʳ : RightCongruent \\
      \\-congʳ y≈z = \\-cong y≈z refl

      //-congˡ : LeftCongruent //
      //-congˡ y≈z = //-cong refl y≈z

      //-congʳ : RightCongruent //
      //-congʳ y≈z = //-cong y≈z refl

      leftDividesˡ : LeftDividesˡ ∙ \\
      leftDividesˡ = proj₁ leftDivides

      leftDividesʳ : LeftDividesʳ ∙ \\
      leftDividesʳ = proj₂ leftDivides

      rightDividesˡ : RightDividesˡ ∙ //
      rightDividesˡ = proj₁ rightDivides

      rightDividesʳ : RightDividesʳ ∙ //
      rightDividesʳ = proj₂ rightDivides

    record IsLoop (∙ \\ // : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
      field
        isQuasigroup : IsQuasigroup ∙ \\ //
        identity     : Identity ε ∙

      open IsQuasigroup isQuasigroup public

      identityˡ : LeftIdentity ε ∙
      identityˡ = proj₁ identity

      identityʳ : RightIdentity ε ∙
      identityʳ = proj₂ identity

    record IsLeftBolLoop (∙ \\ // : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
      field
        isLoop  : IsLoop ∙ \\ //  ε
        leftBol : LeftBol ∙

      open IsLoop isLoop public

    record IsRightBolLoop (∙ \\ // : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
      field
        isLoop   : IsLoop ∙ \\ //  ε
        rightBol : RightBol ∙

      open IsLoop isLoop public

    record IsMoufangLoop (∙ \\ // : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
      field
        isLeftBolLoop  : IsLeftBolLoop ∙ \\ //  ε
        rightBol       : RightBol ∙
        identical      : Identical ∙

      open IsLeftBolLoop isLeftBolLoop public

    record IsMiddleBolLoop (∙ \\ // : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
      field
        isLoop    : IsLoop ∙ \\ //  ε
        middleBol : MiddleBol ∙ \\ //

      open IsLoop isLoop public