diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda
index 88b195ec7d..bbc58e7680 100644
--- a/src/Algebra/Bundles.agda
+++ b/src/Algebra/Bundles.agda
@@ -39,7 +39,7 @@ record SuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) where
     zero#            : Carrier
     isSuccessorSet   : IsSuccessorSet _≈_ suc# zero#
 
-  open IsSuccessorSet isSuccessorSet public
+  open IsSuccessorSet _≈_ isSuccessorSet public
 
   rawSuccessorSet : RawSuccessorSet _ _
   rawSuccessorSet = record { _≈_ = _≈_; suc# = suc#; zero# = zero# }
@@ -59,7 +59,7 @@ record Magma c ℓ : Set (suc (c ⊔ ℓ)) where
     _∙_     : Op₂ Carrier
     isMagma : IsMagma _≈_ _∙_
 
-  open IsMagma isMagma public
+  open IsMagma _≈_ isMagma public
 
   rawMagma : RawMagma _ _
   rawMagma = record { _≈_ = _≈_; _∙_ = _∙_ }
@@ -77,7 +77,7 @@ record SelectiveMagma c ℓ : Set (suc (c ⊔ ℓ)) where
     _∙_              : Op₂ Carrier
     isSelectiveMagma : IsSelectiveMagma _≈_ _∙_
 
-  open IsSelectiveMagma isSelectiveMagma public
+  open IsSelectiveMagma _≈_ isSelectiveMagma public
 
   magma : Magma c ℓ
   magma = record { isMagma = isMagma }
@@ -94,7 +94,7 @@ record CommutativeMagma c ℓ : Set (suc (c ⊔ ℓ)) where
     _∙_                : Op₂ Carrier
     isCommutativeMagma : IsCommutativeMagma _≈_ _∙_
 
-  open IsCommutativeMagma isCommutativeMagma public
+  open IsCommutativeMagma _≈_ isCommutativeMagma public
 
   magma : Magma c ℓ
   magma = record { isMagma = isMagma }
@@ -110,7 +110,7 @@ record IdempotentMagma c ℓ : Set (suc (c ⊔ ℓ)) where
     _∙_     : Op₂ Carrier
     isIdempotentMagma  : IsIdempotentMagma _≈_ _∙_
 
-  open IsIdempotentMagma isIdempotentMagma public
+  open IsIdempotentMagma _≈_ isIdempotentMagma public
 
   magma : Magma c ℓ
   magma = record { isMagma = isMagma }
@@ -127,7 +127,7 @@ record AlternativeMagma c ℓ : Set (suc (c ⊔ ℓ)) where
     _∙_     : Op₂ Carrier
     isAlternativeMagma  : IsAlternativeMagma _≈_ _∙_
 
-  open IsAlternativeMagma isAlternativeMagma public
+  open IsAlternativeMagma _≈_ isAlternativeMagma public
 
   magma : Magma c ℓ
   magma = record { isMagma = isMagma }
@@ -144,7 +144,7 @@ record FlexibleMagma c ℓ : Set (suc (c ⊔ ℓ)) where
     _∙_     : Op₂ Carrier
     isFlexibleMagma  : IsFlexibleMagma _≈_ _∙_
 
-  open IsFlexibleMagma isFlexibleMagma public
+  open IsFlexibleMagma _≈_ isFlexibleMagma public
 
   magma : Magma c ℓ
   magma = record { isMagma = isMagma }
@@ -161,7 +161,7 @@ record MedialMagma c ℓ : Set (suc (c ⊔ ℓ)) where
     _∙_     : Op₂ Carrier
     isMedialMagma  : IsMedialMagma _≈_ _∙_
 
-  open IsMedialMagma isMedialMagma public
+  open IsMedialMagma _≈_ isMedialMagma public
 
   magma : Magma c ℓ
   magma = record { isMagma = isMagma }
@@ -178,7 +178,7 @@ record SemimedialMagma c ℓ : Set (suc (c ⊔ ℓ)) where
     _∙_     : Op₂ Carrier
     isSemimedialMagma  : IsSemimedialMagma _≈_ _∙_
 
-  open IsSemimedialMagma isSemimedialMagma public
+  open IsSemimedialMagma _≈_ isSemimedialMagma public
 
   magma : Magma c ℓ
   magma = record { isMagma = isMagma }
@@ -196,7 +196,7 @@ record Semigroup c ℓ : Set (suc (c ⊔ ℓ)) where
     _∙_         : Op₂ Carrier
     isSemigroup : IsSemigroup _≈_ _∙_
 
-  open IsSemigroup isSemigroup public
+  open IsSemigroup _≈_ isSemigroup public
 
   magma : Magma c ℓ
   magma = record { isMagma = isMagma }
@@ -214,7 +214,7 @@ record Band c ℓ : Set (suc (c ⊔ ℓ)) where
     _∙_     : Op₂ Carrier
     isBand  : IsBand _≈_ _∙_
 
-  open IsBand isBand public
+  open IsBand _≈_ isBand public
 
   semigroup : Semigroup c ℓ
   semigroup = record { isSemigroup = isSemigroup }
@@ -232,7 +232,7 @@ record CommutativeSemigroup c ℓ : Set (suc (c ⊔ ℓ)) where
     _∙_                     : Op₂ Carrier
     isCommutativeSemigroup  : IsCommutativeSemigroup _≈_ _∙_
 
-  open IsCommutativeSemigroup isCommutativeSemigroup public
+  open IsCommutativeSemigroup _≈_ isCommutativeSemigroup public
 
   semigroup : Semigroup c ℓ
   semigroup = record { isSemigroup = isSemigroup }
@@ -252,7 +252,7 @@ record CommutativeBand c ℓ : Set (suc (c ⊔ ℓ)) where
     _∙_                : Op₂ Carrier
     isCommutativeBand  : IsCommutativeBand _≈_ _∙_
 
-  open IsCommutativeBand isCommutativeBand public
+  open IsCommutativeBand _≈_ isCommutativeBand public
 
   band : Band _ _
   band = record { isBand = isBand }
@@ -281,7 +281,7 @@ record UnitalMagma c ℓ : Set (suc (c ⊔ ℓ)) where
     ε        : Carrier
     isUnitalMagma : IsUnitalMagma _≈_ _∙_ ε
 
-  open IsUnitalMagma isUnitalMagma public
+  open IsUnitalMagma _≈_ isUnitalMagma public
 
   magma : Magma c ℓ
   magma = record { isMagma = isMagma }
@@ -300,7 +300,7 @@ record Monoid c ℓ : Set (suc (c ⊔ ℓ)) where
     ε        : Carrier
     isMonoid : IsMonoid _≈_ _∙_ ε
 
-  open IsMonoid isMonoid public
+  open IsMonoid _≈_ isMonoid public
 
   semigroup : Semigroup _ _
   semigroup = record { isSemigroup = isSemigroup }
@@ -325,7 +325,7 @@ record CommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
     ε                   : Carrier
     isCommutativeMonoid : IsCommutativeMonoid _≈_ _∙_ ε
 
-  open IsCommutativeMonoid isCommutativeMonoid public
+  open IsCommutativeMonoid _≈_ isCommutativeMonoid public
 
   monoid : Monoid _ _
   monoid = record { isMonoid = isMonoid }
@@ -349,7 +349,7 @@ record IdempotentMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
     ε                  : Carrier
     isIdempotentMonoid : IsIdempotentMonoid _≈_ _∙_ ε
 
-  open IsIdempotentMonoid isIdempotentMonoid public
+  open IsIdempotentMonoid _≈_ isIdempotentMonoid public
 
   monoid : Monoid _ _
   monoid = record { isMonoid = isMonoid }
@@ -371,7 +371,7 @@ record IdempotentCommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
     ε                             : Carrier
     isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid _≈_ _∙_ ε
 
-  open IsIdempotentCommutativeMonoid isIdempotentCommutativeMonoid public
+  open IsIdempotentCommutativeMonoid _≈_ isIdempotentCommutativeMonoid public
 
   commutativeMonoid : CommutativeMonoid _ _
   commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }
@@ -418,7 +418,7 @@ record InvertibleMagma c ℓ : Set (suc (c ⊔ ℓ)) where
     _⁻¹     : Op₁ Carrier
     isInvertibleMagma : IsInvertibleMagma _≈_ _∙_ ε _⁻¹
 
-  open IsInvertibleMagma isInvertibleMagma public
+  open IsInvertibleMagma _≈_ isInvertibleMagma public
 
   magma : Magma _ _
   magma = record { isMagma = isMagma }
@@ -439,7 +439,7 @@ record InvertibleUnitalMagma c ℓ : Set (suc (c ⊔ ℓ)) where
     _⁻¹                      : Op₁ Carrier
     isInvertibleUnitalMagma  : IsInvertibleUnitalMagma _≈_ _∙_ ε _⁻¹
 
-  open IsInvertibleUnitalMagma isInvertibleUnitalMagma public
+  open IsInvertibleUnitalMagma _≈_ isInvertibleUnitalMagma public
 
   invertibleMagma : InvertibleMagma _ _
   invertibleMagma = record { isInvertibleMagma = isInvertibleMagma }
@@ -459,7 +459,7 @@ record Group c ℓ : Set (suc (c ⊔ ℓ)) where
     _⁻¹     : Op₁ Carrier
     isGroup : IsGroup _≈_ _∙_ ε _⁻¹
 
-  open IsGroup isGroup public
+  open IsGroup _≈_ isGroup public
 
   rawGroup : RawGroup _ _
   rawGroup = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε; _⁻¹ = _⁻¹}
@@ -492,7 +492,7 @@ record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where
     _⁻¹            : Op₁ Carrier
     isAbelianGroup : IsAbelianGroup _≈_ _∙_ ε _⁻¹
 
-  open IsAbelianGroup isAbelianGroup public
+  open IsAbelianGroup _≈_ isAbelianGroup public
 
   group : Group _ _
   group = record { isGroup = isGroup }
@@ -1139,9 +1139,9 @@ record Quasigroup c ℓ : Set (suc (c ⊔ ℓ)) where
     _∙_          : Op₂ Carrier
     _\\_         : Op₂ Carrier
     _//_         : Op₂ Carrier
-    isQuasigroup : IsQuasigroup  _≈_ _∙_ _\\_ _//_
+    isQuasigroup : IsQuasigroup _≈_ _∙_ _\\_ _//_
 
-  open IsQuasigroup isQuasigroup public
+  open IsQuasigroup _≈_ isQuasigroup public
 
   magma : Magma c ℓ
   magma = record { isMagma = isMagma }
@@ -1174,7 +1174,7 @@ record Loop  c ℓ : Set (suc (c ⊔ ℓ)) where
     ε       : Carrier
     isLoop  : IsLoop  _≈_ _∙_ _\\_ _//_ ε
 
-  open IsLoop isLoop public
+  open IsLoop _≈_ isLoop public
 
   rawLoop : RawLoop c ℓ
   rawLoop = record
@@ -1205,7 +1205,7 @@ record LeftBolLoop c ℓ : Set (suc (c ⊔ ℓ)) where
     ε       : Carrier
     isLeftBolLoop : IsLeftBolLoop  _≈_ _∙_ _\\_ _//_ ε
 
-  open IsLeftBolLoop isLeftBolLoop public
+  open IsLeftBolLoop _≈_ isLeftBolLoop public
 
   loop : Loop _ _
   loop = record { isLoop = isLoop }
@@ -1227,7 +1227,7 @@ record RightBolLoop c ℓ : Set (suc (c ⊔ ℓ)) where
     ε       : Carrier
     isRightBolLoop : IsRightBolLoop  _≈_ _∙_ _\\_ _//_ ε
 
-  open IsRightBolLoop isRightBolLoop public
+  open IsRightBolLoop _≈_ isRightBolLoop public
 
   loop : Loop _ _
   loop = record { isLoop = isLoop }
@@ -1249,7 +1249,7 @@ record MoufangLoop c ℓ : Set (suc (c ⊔ ℓ)) where
     ε       : Carrier
     isMoufangLoop : IsMoufangLoop  _≈_ _∙_ _\\_ _//_ ε
 
-  open IsMoufangLoop isMoufangLoop public
+  open IsMoufangLoop _≈_ isMoufangLoop public
 
   leftBolLoop : LeftBolLoop _ _
   leftBolLoop = record { isLeftBolLoop = isLeftBolLoop }
@@ -1271,11 +1271,10 @@ record MiddleBolLoop c ℓ : Set (suc (c ⊔ ℓ)) where
     ε               : Carrier
     isMiddleBolLoop : IsMiddleBolLoop  _≈_ _∙_ _\\_ _//_ ε
 
-  open IsMiddleBolLoop isMiddleBolLoop public
+  open IsMiddleBolLoop _≈_ isMiddleBolLoop public
 
   loop : Loop _ _
   loop = record { isLoop = isLoop }
 
   open Loop loop public
     using (quasigroup)
-
diff --git a/src/Algebra/Properties/Group.agda b/src/Algebra/Properties/Group.agda
index 8277f4feb7..d9e0d15c0d 100644
--- a/src/Algebra/Properties/Group.agda
+++ b/src/Algebra/Properties/Group.agda
@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Some derivable properties
+-- Shim for lemmas re-exported from Algebra.Properties.IsGroup
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
@@ -10,161 +10,5 @@ open import Algebra.Bundles
 
 module Algebra.Properties.Group {g₁ g₂} (G : Group g₁ g₂) where
 
-import Algebra.Properties.Loop as LoopProperties
-import Algebra.Properties.Quasigroup as QuasigroupProperties
-open import Data.Product.Base using (_,_)
-open import Function.Base using (_$_)
-open import Function.Definitions using (Injective)
-
-open Group G
-open import Algebra.Consequences.Setoid setoid
-open import Algebra.Definitions _≈_
-open import Algebra.Structures _≈_ using (IsLoop; IsQuasigroup)
-open import Relation.Binary.Reasoning.Setoid setoid
-
-\\-cong₂ : Congruent₂ _\\_
-\\-cong₂ x≈y u≈v = ∙-cong (⁻¹-cong x≈y) u≈v
-
-//-cong₂ : Congruent₂ _//_
-//-cong₂ x≈y u≈v = ∙-cong x≈y (⁻¹-cong u≈v)
-
-------------------------------------------------------------------------
--- Groups are quasi-groups
-
-\\-leftDividesˡ : LeftDividesˡ _∙_ _\\_
-\\-leftDividesˡ x y = begin
-  x  ∙ (x \\ y)  ≈⟨ assoc x (x ⁻¹) y ⟨
-  x ∙ x ⁻¹ ∙ y   ≈⟨ ∙-congʳ (inverseʳ x) ⟩
-  ε ∙ y          ≈⟨ identityˡ y ⟩
-  y              ∎
-
-\\-leftDividesʳ : LeftDividesʳ _∙_ _\\_
-\\-leftDividesʳ x y = begin
-  x \\ x ∙ y     ≈⟨ assoc (x ⁻¹) x y ⟨
-  x ⁻¹ ∙ x ∙ y   ≈⟨ ∙-congʳ (inverseˡ x) ⟩
-  ε ∙ y          ≈⟨ identityˡ y ⟩
-  y              ∎
-
-
-\\-leftDivides : LeftDivides _∙_ _\\_
-\\-leftDivides = \\-leftDividesˡ , \\-leftDividesʳ
-
-//-rightDividesˡ : RightDividesˡ _∙_ _//_
-//-rightDividesˡ x y = begin
-  (y // x) ∙ x    ≈⟨ assoc y (x ⁻¹) x ⟩
-  y ∙ (x ⁻¹ ∙ x)  ≈⟨ ∙-congˡ (inverseˡ x) ⟩
-  y ∙ ε           ≈⟨ identityʳ y ⟩
-  y               ∎
-
-//-rightDividesʳ : RightDividesʳ _∙_ _//_
-//-rightDividesʳ x y = begin
-  y ∙ x // x    ≈⟨ assoc y x (x ⁻¹) ⟩
-  y ∙ (x // x)  ≈⟨ ∙-congˡ (inverseʳ x) ⟩
-  y ∙ ε         ≈⟨ identityʳ y ⟩
-  y             ∎
-
-//-rightDivides : RightDivides _∙_ _//_
-//-rightDivides = //-rightDividesˡ , //-rightDividesʳ
-
-isQuasigroup : IsQuasigroup _∙_ _\\_ _//_
-isQuasigroup = record
-  { isMagma = isMagma
-  ; \\-cong = \\-cong₂
-  ; //-cong = //-cong₂
-  ; leftDivides = \\-leftDivides
-  ; rightDivides = //-rightDivides
-  }
-
-quasigroup : Quasigroup _ _
-quasigroup = record { isQuasigroup = isQuasigroup }
-
-open QuasigroupProperties quasigroup public
-  using (x≈z//y; y≈x\\z)
-  renaming (cancelˡ to ∙-cancelˡ; cancelʳ to ∙-cancelʳ; cancel to ∙-cancel)
-
-------------------------------------------------------------------------
--- Groups are loops
-
-isLoop : IsLoop _∙_ _\\_ _//_ ε
-isLoop = record { isQuasigroup = isQuasigroup ; identity = identity }
-
-loop : Loop _ _
-loop = record { isLoop = isLoop }
-
-open LoopProperties loop public
-  using (identityˡ-unique; identityʳ-unique; identity-unique)
-
-------------------------------------------------------------------------
--- Other properties
-
-inverseˡ-unique : ∀ x y → x ∙ y ≈ ε → x ≈ y ⁻¹
-inverseˡ-unique x y eq = trans (x≈z//y x y ε eq) (identityˡ _)
-
-inverseʳ-unique : ∀ x y → x ∙ y ≈ ε → y ≈ x ⁻¹
-inverseʳ-unique x y eq = trans (y≈x\\z x y ε eq) (identityʳ _)
-
-ε⁻¹≈ε : ε ⁻¹ ≈ ε
-ε⁻¹≈ε = sym $ inverseˡ-unique _ _ (identityˡ ε)
-
-⁻¹-selfInverse : SelfInverse _⁻¹
-⁻¹-selfInverse {x} {y} eq = sym $ inverseˡ-unique x y $ begin
-  x ∙ y    ≈⟨ ∙-congˡ eq ⟨
-  x ∙ x ⁻¹ ≈⟨ inverseʳ x  ⟩
-  ε        ∎
-
-⁻¹-involutive : Involutive _⁻¹
-⁻¹-involutive = selfInverse⇒involutive ⁻¹-selfInverse
-
-x∙y⁻¹≈ε⇒x≈y : ∀ x y → (x ∙ y ⁻¹) ≈ ε → x ≈ y
-x∙y⁻¹≈ε⇒x≈y x y x∙y⁻¹≈ε = begin
-  x         ≈⟨ inverseˡ-unique x (y ⁻¹) x∙y⁻¹≈ε ⟩
-  y ⁻¹ ⁻¹   ≈⟨ ⁻¹-involutive y ⟩
-  y         ∎
-
-x≈y⇒x∙y⁻¹≈ε : ∀ {x y} → x ≈ y → (x ∙ y ⁻¹) ≈ ε
-x≈y⇒x∙y⁻¹≈ε {x} {y} x≈y = begin
-  x ∙ y ⁻¹ ≈⟨ ∙-congʳ x≈y ⟩
-  y ∙ y ⁻¹ ≈⟨ inverseʳ y ⟩
-  ε        ∎
-
-⁻¹-injective : Injective _≈_ _≈_ _⁻¹
-⁻¹-injective = selfInverse⇒injective ⁻¹-selfInverse
-
-⁻¹-anti-homo-∙ : ∀ x y → (x ∙ y) ⁻¹ ≈ y ⁻¹ ∙ x ⁻¹
-⁻¹-anti-homo-∙ x y = ∙-cancelˡ _ _ _ $ begin
-  x ∙ y ∙ (x ∙ y) ⁻¹    ≈⟨ inverseʳ _ ⟩
-  ε                     ≈⟨ inverseʳ _ ⟨
-  x ∙ x ⁻¹              ≈⟨ ∙-congʳ (//-rightDividesʳ y x) ⟨
-  (x ∙ y) ∙ y ⁻¹ ∙ x ⁻¹ ≈⟨ assoc (x ∙ y) (y ⁻¹) (x ⁻¹) ⟩
-  x ∙ y ∙ (y ⁻¹ ∙ x ⁻¹) ∎
-
-⁻¹-anti-homo-// : ∀ x y → (x // y) ⁻¹ ≈ y // x
-⁻¹-anti-homo-// x y = begin
-  (x // y) ⁻¹      ≡⟨⟩
-  (x ∙ y ⁻¹) ⁻¹    ≈⟨ ⁻¹-anti-homo-∙ x (y ⁻¹) ⟩
-  (y ⁻¹) ⁻¹ ∙ x ⁻¹ ≈⟨ ∙-congʳ (⁻¹-involutive y) ⟩
-  y ∙ x ⁻¹         ≡⟨⟩
-  y // x ∎
-
-⁻¹-anti-homo-\\ : ∀ x y → (x \\ y) ⁻¹ ≈ y \\ x
-⁻¹-anti-homo-\\ x y = begin
-  (x \\ y) ⁻¹      ≡⟨⟩
-  (x ⁻¹ ∙ y) ⁻¹    ≈⟨ ⁻¹-anti-homo-∙ (x ⁻¹) y ⟩
-  y ⁻¹ ∙ (x ⁻¹) ⁻¹ ≈⟨ ∙-congˡ (⁻¹-involutive x) ⟩
-  y ⁻¹ ∙ x         ≡⟨⟩
-  y \\ x ∎
-
-\\≗flip-//⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_
-\\≗flip-//⇒comm \\≗//ᵒ x y = begin
-  x ∙ y                ≈⟨ ∙-congˡ (//-rightDividesˡ x y) ⟨
-  x ∙ ((y // x) ∙ x)   ≈⟨ ∙-congˡ (∙-congʳ (\\≗//ᵒ x y)) ⟨
-  x ∙ ((x \\ y) ∙ x)   ≈⟨ assoc x (x \\ y) x ⟨
-  x ∙ (x \\ y) ∙ x     ≈⟨ ∙-congʳ (\\-leftDividesˡ x y) ⟩
-  y ∙ x                ∎
-
-comm⇒\\≗flip-// : Commutative _∙_ → ∀ x y → x \\ y ≈ y // x
-comm⇒\\≗flip-// comm x y = begin
-  x \\ y    ≡⟨⟩
-  x ⁻¹ ∙ y  ≈⟨ comm _ _ ⟩
-  y ∙ x ⁻¹  ≡⟨⟩
-  y // x    ∎
+open Group G using (isGroup)
+open import Algebra.Properties.IsGroup isGroup public
diff --git a/src/Algebra/Properties/IsGroup.agda b/src/Algebra/Properties/IsGroup.agda
new file mode 100644
index 0000000000..6ba83097c3
--- /dev/null
+++ b/src/Algebra/Properties/IsGroup.agda
@@ -0,0 +1,115 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some derivable properties
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Core using (Rel)
+open import Algebra.Core using (Op₁; Op₂)
+open import Algebra.Structures.IsGroup using (IsGroup)
+
+module Algebra.Properties.IsGroup
+  {a ℓ} {A} {_≈_} {_∙_} {ε} {_⁻¹}
+  (isGroup : IsGroup {a = a} {ℓ = ℓ} {A = A} _≈_ _∙_ ε _⁻¹)
+  where
+
+open import Data.Product.Base using (_,_)
+open import Function.Base using (_$_)
+open import Function.Definitions using (Injective)
+
+open IsGroup isGroup
+open import Algebra.Consequences.Setoid setoid
+open import Algebra.Definitions _≈_
+import Algebra.Properties.IsLoop as LoopProperties
+import Algebra.Properties.IsQuasigroup as QuasigroupProperties
+open import Relation.Binary.Reasoning.Setoid setoid
+
+------------------------------------------------------------------------
+-- Groups are quasi-groups
+
+open QuasigroupProperties isQuasigroup public
+  using (x≈z//y; y≈x\\z)
+  renaming (cancelˡ to ∙-cancelˡ; cancelʳ to ∙-cancelʳ; cancel to ∙-cancel)
+
+------------------------------------------------------------------------
+-- Groups are loops
+
+open LoopProperties isLoop public
+  using (identityˡ-unique; identityʳ-unique; identity-unique)
+
+------------------------------------------------------------------------
+-- Other properties
+
+inverseˡ-unique : ∀ x y → (x ∙ y) ≈ ε → x ≈ (y ⁻¹)
+inverseˡ-unique x y eq = trans (x≈z//y x y ε eq) (identityˡ _)
+
+inverseʳ-unique : ∀ x y → (x ∙ y) ≈ ε → y ≈ (x ⁻¹)
+inverseʳ-unique x y eq = trans (y≈x\\z x y ε eq) (identityʳ _)
+
+ε⁻¹≈ε : (ε ⁻¹) ≈ ε
+ε⁻¹≈ε = sym $ inverseˡ-unique _ _ (identityˡ ε)
+
+⁻¹-selfInverse : SelfInverse _⁻¹
+⁻¹-selfInverse {x} {y} eq = sym $ inverseˡ-unique x y $ begin
+  x ∙ y    ≈⟨ ∙-congˡ eq ⟨
+  x ∙ (x ⁻¹) ≈⟨ inverseʳ x  ⟩
+  ε        ∎
+
+⁻¹-involutive : Involutive _⁻¹
+⁻¹-involutive = selfInverse⇒involutive ⁻¹-selfInverse
+
+x∙y⁻¹≈ε⇒x≈y : ∀ x y → (x ∙ (y ⁻¹)) ≈ ε → x ≈ y
+x∙y⁻¹≈ε⇒x≈y x y x∙y⁻¹≈ε = begin
+  x         ≈⟨ inverseˡ-unique x (y ⁻¹) x∙y⁻¹≈ε ⟩
+  (y ⁻¹) ⁻¹   ≈⟨ ⁻¹-involutive y ⟩
+  y         ∎
+
+x≈y⇒x∙y⁻¹≈ε : ∀ {x y} → x ≈ y → (x ∙ (y ⁻¹)) ≈ ε
+x≈y⇒x∙y⁻¹≈ε {x} {y} x≈y = begin
+  x ∙ (y ⁻¹) ≈⟨ ∙-congʳ x≈y ⟩
+  y ∙ (y ⁻¹) ≈⟨ inverseʳ y ⟩
+  ε        ∎
+
+⁻¹-injective : Injective _≈_ _≈_ _⁻¹
+⁻¹-injective = selfInverse⇒injective ⁻¹-selfInverse
+
+⁻¹-anti-homo-∙ : ∀ x y → ((x ∙ y) ⁻¹) ≈ ((y ⁻¹) ∙ (x ⁻¹))
+⁻¹-anti-homo-∙ x y = ∙-cancelˡ _ _ _ $ begin
+  (x ∙ y) ∙ ((x ∙ y) ⁻¹)    ≈⟨ inverseʳ _ ⟩
+  ε                     ≈⟨ inverseʳ _ ⟨
+  x ∙ (x ⁻¹)              ≈⟨ ∙-congʳ (//-rightDividesʳ y x) ⟨
+  ((x ∙ y) ∙ (y ⁻¹)) ∙ (x ⁻¹) ≈⟨ assoc (x ∙ y) (y ⁻¹) (x ⁻¹) ⟩
+  (x ∙ y) ∙ ((y ⁻¹) ∙ (x ⁻¹)) ∎
+
+⁻¹-anti-homo-// : ∀ x y → ((x // y) ⁻¹) ≈ (y // x)
+⁻¹-anti-homo-// x y = begin
+  (x // y) ⁻¹      ≡⟨⟩
+  (x ∙ (y ⁻¹)) ⁻¹    ≈⟨ ⁻¹-anti-homo-∙ x (y ⁻¹) ⟩
+  ((y ⁻¹) ⁻¹) ∙ (x ⁻¹) ≈⟨ ∙-congʳ (⁻¹-involutive y) ⟩
+  y ∙ (x ⁻¹)         ≡⟨⟩
+  y // x ∎
+
+⁻¹-anti-homo-\\ : ∀ x y → ((x \\ y) ⁻¹) ≈ (y \\ x)
+⁻¹-anti-homo-\\ x y = begin
+  (x \\ y) ⁻¹      ≡⟨⟩
+  ((x ⁻¹) ∙ y) ⁻¹    ≈⟨ ⁻¹-anti-homo-∙ (x ⁻¹) y ⟩
+  (y ⁻¹) ∙ ((x ⁻¹) ⁻¹) ≈⟨ ∙-congˡ (⁻¹-involutive x) ⟩
+  (y ⁻¹) ∙ x         ≡⟨⟩
+  y \\ x ∎
+
+\\≗flip-//⇒comm : (∀ x y → (x \\ y) ≈ (y // x)) → Commutative _∙_
+\\≗flip-//⇒comm \\≗//ᵒ x y = begin
+  x ∙ y                ≈⟨ ∙-congˡ (//-rightDividesˡ x y) ⟨
+  x ∙ ((y // x) ∙ x)   ≈⟨ ∙-congˡ (∙-congʳ (\\≗//ᵒ x y)) ⟨
+  x ∙ ((x \\ y) ∙ x)   ≈⟨ assoc x (x \\ y) x ⟨
+  (x ∙ (x \\ y)) ∙ x     ≈⟨ ∙-congʳ (\\-leftDividesˡ x y) ⟩
+  y ∙ x                ∎
+
+comm⇒\\≗flip-// : Commutative _∙_ → ∀ x y → (x \\ y) ≈ (y // x)
+comm⇒\\≗flip-// comm x y = begin
+  x \\ y    ≡⟨⟩
+  (x ⁻¹) ∙ y  ≈⟨ comm _ _ ⟩
+  y ∙ (x ⁻¹)  ≡⟨⟩
+  y // x    ∎
diff --git a/src/Algebra/Properties/IsLoop.agda b/src/Algebra/Properties/IsLoop.agda
new file mode 100644
index 0000000000..73f39dd395
--- /dev/null
+++ b/src/Algebra/Properties/IsLoop.agda
@@ -0,0 +1,60 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some basic properties of Loops
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Structures.IsQuasigroup using (IsLoop)
+
+module Algebra.Properties.IsLoop
+  {a ℓ} {A} {_≈_} {_∙_ _\\_ _//_} {ε}
+  (isLoop : IsLoop {a = a} {ℓ = ℓ} {A = A} _≈_ _∙_ _\\_ _//_ ε) where
+
+open import Algebra.Definitions _≈_
+open import Data.Product.Base using (proj₂)
+
+open IsLoop isLoop
+open import Algebra.Properties.IsQuasigroup isQuasigroup
+open import Relation.Binary.Reasoning.Setoid setoid
+
+x//x≈ε : ∀ x → (x // x) ≈ ε
+x//x≈ε x = begin
+  x // x       ≈⟨ //-congʳ (identityˡ x) ⟨
+  (ε ∙ x) // x ≈⟨ rightDividesʳ x ε ⟩
+  ε            ∎
+
+x\\x≈ε : ∀ x → (x \\ x) ≈ ε
+x\\x≈ε x = begin
+  x \\ x       ≈⟨ \\-congˡ (identityʳ x ) ⟨
+  x \\ (x ∙ ε) ≈⟨ leftDividesʳ x ε ⟩
+  ε            ∎
+
+ε\\x≈x : ∀ x → (ε \\ x) ≈ x
+ε\\x≈x x = begin
+  ε \\ x       ≈⟨ identityˡ (ε \\ x) ⟨
+  ε ∙ (ε \\ x) ≈⟨ leftDividesˡ ε x ⟩
+  x            ∎
+
+x//ε≈x : ∀ x → (x // ε) ≈ x
+x//ε≈x x = begin
+ x // ε       ≈⟨ identityʳ (x // ε) ⟨
+ (x // ε) ∙ ε ≈⟨ rightDividesˡ ε x ⟩
+ x            ∎
+
+identityˡ-unique : ∀ x y → (x ∙ y) ≈ y → x ≈ ε
+identityˡ-unique x y eq = begin
+  x      ≈⟨ x≈z//y x y y eq ⟩
+  y // y ≈⟨ x//x≈ε y ⟩
+  ε      ∎
+
+identityʳ-unique : ∀ x y → (x ∙ y) ≈ x → y ≈ ε
+identityʳ-unique x y eq = begin
+  y       ≈⟨ y≈x\\z x y x eq ⟩
+  x \\ x  ≈⟨ x\\x≈ε x ⟩
+  ε       ∎
+
+identity-unique : ∀ {x} → Identity x _∙_ → x ≈ ε
+identity-unique {x} id = identityˡ-unique x x (proj₂ id x)
+
diff --git a/src/Algebra/Properties/IsMagma.agda b/src/Algebra/Properties/IsMagma.agda
new file mode 100644
index 0000000000..f8efc6cb1d
--- /dev/null
+++ b/src/Algebra/Properties/IsMagma.agda
@@ -0,0 +1,22 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some theory for Semigroup
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Core using (Rel)
+open import Algebra.Core using (Op₂)
+open import Algebra.Structures.IsMagma using (IsMagma)
+
+module Algebra.Properties.IsMagma
+  {a ℓ} {A} {_≈_} {_∙_} (isMagma : IsMagma {a = a} {ℓ = ℓ} {A = A} _≈_ _∙_)
+  where
+
+open import Algebra.Definitions _≈_
+  using (Alternative; LeftAlternative; RightAlternative; Flexible)
+open import Data.Product.Base using (_,_)
+
+open IsMagma isMagma
+  using (setoid; trans ; refl; sym; ∙-cong; ∙-congˡ; ∙-congʳ)
diff --git a/src/Algebra/Properties/IsQuasigroup.agda b/src/Algebra/Properties/IsQuasigroup.agda
new file mode 100644
index 0000000000..4a0f2f38f6
--- /dev/null
+++ b/src/Algebra/Properties/IsQuasigroup.agda
@@ -0,0 +1,48 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some basic properties of Quasigroups
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Structures.IsQuasigroup using (IsQuasigroup)
+
+module Algebra.Properties.IsQuasigroup
+  {a ℓ} {A} {_≈_} {_∙_ _\\_ _//_}
+  (isQuasigroup : IsQuasigroup {a = a} {ℓ} {A = A}_≈_ _∙_ _\\_ _//_) where
+
+open import Algebra.Definitions _≈_
+open import Data.Product.Base using (_,_)
+
+open IsQuasigroup isQuasigroup
+open import Relation.Binary.Reasoning.Setoid setoid
+
+cancelˡ : LeftCancellative _∙_
+cancelˡ x y z eq = begin
+  y             ≈⟨ leftDividesʳ x y ⟨
+  x \\ (x ∙ y)  ≈⟨ \\-congˡ eq ⟩
+  x \\ (x ∙ z)  ≈⟨ leftDividesʳ x z ⟩
+  z             ∎
+
+cancelʳ : RightCancellative _∙_
+cancelʳ x y z eq = begin
+  y             ≈⟨ rightDividesʳ x y ⟨
+  (y ∙ x) // x  ≈⟨ //-congʳ eq ⟩
+  (z ∙ x) // x  ≈⟨ rightDividesʳ x z ⟩
+  z             ∎
+
+cancel : Cancellative _∙_
+cancel = cancelˡ , cancelʳ
+
+y≈x\\z : ∀ x y z → (x ∙ y) ≈ z → y ≈ (x \\ z)
+y≈x\\z x y z eq = begin
+  y            ≈⟨ leftDividesʳ x y ⟨
+  x \\ (x ∙ y) ≈⟨ \\-congˡ eq ⟩
+  x \\ z       ∎
+
+x≈z//y : ∀ x y z → (x ∙ y) ≈ z → x ≈ (z // y)
+x≈z//y x y z eq = begin
+  x            ≈⟨ rightDividesʳ y x ⟨
+  (x ∙ y) // y ≈⟨ //-congʳ eq ⟩
+  z // y       ∎
diff --git a/src/Algebra/Properties/IsSemigroup.agda b/src/Algebra/Properties/IsSemigroup.agda
new file mode 100644
index 0000000000..ef3f4b36ff
--- /dev/null
+++ b/src/Algebra/Properties/IsSemigroup.agda
@@ -0,0 +1,51 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some theory for Semigroup
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Core using (Rel)
+open import Algebra.Core using (Op₂)
+open import Algebra.Structures.IsSemigroup using (IsSemigroup)
+
+module Algebra.Properties.IsSemigroup
+  {a ℓ} {A} {_≈_} {_∙_} (isSemigroup : IsSemigroup {a = a} {ℓ = ℓ} {A = A} _≈_ _∙_)
+  where
+
+open import Algebra.Definitions _≈_
+  using (Alternative; LeftAlternative; RightAlternative; Flexible)
+open import Algebra.Structures.IsMagma _≈_
+  using (IsMagma; IsAlternativeMagma; IsFlexibleMagma)
+open import Data.Product.Base using (_,_)
+
+open IsSemigroup isSemigroup
+  using (setoid; trans ; refl; sym; assoc; ∙-cong; ∙-congˡ; ∙-congʳ; isMagma)
+open import Algebra.Properties.IsMagma isMagma
+
+private
+  variable
+    u v w x y z : A
+
+x∙yz≈xy∙z : ∀ x y z → (x ∙ (y ∙ z)) ≈ ((x ∙ y) ∙ z)
+x∙yz≈xy∙z x y z = sym (assoc x y z)
+
+alternativeˡ : LeftAlternative _∙_
+alternativeˡ x y = assoc x x y
+
+alternativeʳ : RightAlternative _∙_
+alternativeʳ x y = sym (assoc x y y)
+
+alternative : Alternative _∙_
+alternative = alternativeˡ , alternativeʳ
+
+flexible : Flexible _∙_
+flexible x y = assoc x y x
+
+isAlternativeMagma : IsAlternativeMagma _∙_
+isAlternativeMagma = record { isMagma = isMagma ; alter = alternative }
+
+isFlexibleMagma : IsFlexibleMagma _∙_
+isFlexibleMagma = record { isMagma = isMagma ; flex = flexible }
+
diff --git a/src/Algebra/Properties/Loop.agda b/src/Algebra/Properties/Loop.agda
index 46ed1e7f7c..246224ffc4 100644
--- a/src/Algebra/Properties/Loop.agda
+++ b/src/Algebra/Properties/Loop.agda
@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Some basic properties of Loop
+-- Shim for lemmas re-exported from Algebra.Properties.IsLoop
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
@@ -10,48 +10,5 @@ open import Algebra.Bundles using (Loop)
 
 module Algebra.Properties.Loop {l₁ l₂} (L : Loop l₁ l₂) where
 
-open Loop L
-open import Algebra.Definitions _≈_
-open import Algebra.Properties.Quasigroup quasigroup
-open import Data.Product.Base using (proj₂)
-open import Relation.Binary.Reasoning.Setoid setoid
-
-x//x≈ε : ∀ x → x // x ≈ ε
-x//x≈ε x = begin
-  x // x       ≈⟨ //-congʳ (identityˡ x) ⟨
-  (ε ∙ x) // x ≈⟨ rightDividesʳ x ε ⟩
-  ε            ∎
-
-x\\x≈ε : ∀ x → x \\ x ≈ ε
-x\\x≈ε x = begin
-  x \\ x       ≈⟨ \\-congˡ (identityʳ x ) ⟨
-  x \\ (x ∙ ε) ≈⟨ leftDividesʳ x ε ⟩
-  ε            ∎
-
-ε\\x≈x : ∀ x → ε \\ x ≈ x
-ε\\x≈x x = begin
-  ε \\ x       ≈⟨ identityˡ (ε \\ x) ⟨
-  ε ∙ (ε \\ x) ≈⟨ leftDividesˡ ε x ⟩
-  x            ∎
-
-x//ε≈x : ∀ x → x // ε ≈ x
-x//ε≈x x = begin
- x // ε       ≈⟨ identityʳ (x // ε) ⟨
- (x // ε) ∙ ε ≈⟨ rightDividesˡ ε x ⟩
- x            ∎
-
-identityˡ-unique : ∀ x y → x ∙ y ≈ y → x ≈ ε
-identityˡ-unique x y eq = begin
-  x      ≈⟨ x≈z//y x y y eq ⟩
-  y // y ≈⟨ x//x≈ε y ⟩
-  ε      ∎
-
-identityʳ-unique : ∀ x y → x ∙ y ≈ x → y ≈ ε
-identityʳ-unique x y eq = begin
-  y       ≈⟨ y≈x\\z x y x eq ⟩
-  x \\ x  ≈⟨ x\\x≈ε x ⟩
-  ε       ∎
-
-identity-unique : ∀ {x} → Identity x _∙_ → x ≈ ε
-identity-unique {x} id = identityˡ-unique x x (proj₂ id x)
-
+open Loop L using (isLoop)
+open import Algebra.Properties.IsLoop isLoop public
diff --git a/src/Algebra/Properties/Quasigroup.agda b/src/Algebra/Properties/Quasigroup.agda
index e8c7516978..a1cb27ff94 100644
--- a/src/Algebra/Properties/Quasigroup.agda
+++ b/src/Algebra/Properties/Quasigroup.agda
@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Some basic properties of Quasigroup
+-- Shim for lemmas re-exported from Algebra.Properties.IsQuasigroup
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
@@ -10,36 +10,5 @@ open import Algebra.Bundles using (Quasigroup)
 
 module Algebra.Properties.Quasigroup {q₁ q₂} (Q : Quasigroup q₁ q₂) where
 
-open Quasigroup Q
-open import Algebra.Definitions _≈_
-open import Relation.Binary.Reasoning.Setoid setoid
-open import Data.Product.Base using (_,_)
-
-cancelˡ : LeftCancellative _∙_
-cancelˡ x y z eq = begin
-  y             ≈⟨ leftDividesʳ x y ⟨
-  x \\ (x ∙ y)  ≈⟨ \\-congˡ eq ⟩
-  x \\ (x ∙ z)  ≈⟨ leftDividesʳ x z ⟩
-  z             ∎
-
-cancelʳ : RightCancellative _∙_
-cancelʳ x y z eq = begin
-  y             ≈⟨ rightDividesʳ x y ⟨
-  (y ∙ x) // x  ≈⟨ //-congʳ eq ⟩
-  (z ∙ x) // x  ≈⟨ rightDividesʳ x z ⟩
-  z             ∎
-
-cancel : Cancellative _∙_
-cancel = cancelˡ , cancelʳ
-
-y≈x\\z : ∀ x y z → x ∙ y ≈ z → y ≈ x \\ z
-y≈x\\z x y z eq = begin
-  y            ≈⟨ leftDividesʳ x y ⟨
-  x \\ (x ∙ y) ≈⟨ \\-congˡ eq ⟩
-  x \\ z       ∎
-
-x≈z//y : ∀ x y z → x ∙ y ≈ z → x ≈ z // y
-x≈z//y x y z eq = begin
-  x            ≈⟨ rightDividesʳ y x ⟨
-  (x ∙ y) // y ≈⟨ //-congʳ eq ⟩
-  z // y       ∎
+open Quasigroup Q using (isQuasigroup)
+open import Algebra.Properties.IsQuasigroup isQuasigroup public
diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda
index 1b465c6d0f..267851b130 100644
--- a/src/Algebra/Structures.agda
+++ b/src/Algebra/Structures.agda
@@ -18,8 +18,12 @@ module Algebra.Structures
   (_≈_ : Rel A ℓ)    -- The underlying equality relation
   where
 
--- The file is divided into sections depending on the arities of the
--- components of the algebraic structure.
+-- The file now re-exports structures defined in their own submodules,
+-- grouped 'logically' by elaborations on a basic Raw signature, with
+-- some additional redundancy for the sake of existing conventions,
+-- eg. `IsMagma` and `IsSemigroup` share the same `Raw` signature, but
+-- are differentiated because they enjoy different `Properties`.
+-- This may change in subsequent revisions!
 
 open import Algebra.Core using (Op₁; Op₂)
 open import Algebra.Definitions _≈_
@@ -28,340 +32,14 @@ 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)
+-- Re-exports
 
+open import Algebra.Structures.IsSuccessorSet _≈_ public
+open import Algebra.Structures.IsMagma _≈_ public
+open import Algebra.Structures.IsSemigroup _≈_ public
+open import Algebra.Structures.IsMonoid _≈_ public
+open import Algebra.Structures.IsQuasigroup _≈_ public
+open import Algebra.Structures.IsGroup _≈_ public
 
 ------------------------------------------------------------------------
 -- Structures with 2 binary operations & 1 element
@@ -961,84 +639,3 @@ record IsCommutativeRing
     ; *-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
diff --git a/src/Algebra/Structures/IsGroup.agda b/src/Algebra/Structures/IsGroup.agda
new file mode 100644
index 0000000000..9f9fed50d5
--- /dev/null
+++ b/src/Algebra/Structures/IsGroup.agda
@@ -0,0 +1,135 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The structure of a group
+------------------------------------------------------------------------
+
+-- 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)
+
+module Algebra.Structures.IsGroup
+  {a ℓ} {A : Set a}  -- The underlying set
+  (_≈_ : Rel A ℓ)    -- The underlying equality relation
+  where
+
+open import Algebra.Core using (Op₁; Op₂)
+open import Algebra.Definitions _≈_
+open import Algebra.Structures.IsMagma _≈_
+open import Algebra.Structures.IsMonoid _≈_
+open import Algebra.Structures.IsQuasigroup _≈_
+open import Data.Product.Base using (_,_; proj₁; proj₂)
+open import Level using (_⊔_)
+
+------------------------------------------------------------------------
+-- Definition
+
+record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where
+  field
+    isMonoid  : IsMonoid _∙_ ε
+    inverse   : Inverse ε _⁻¹ _∙_
+    ⁻¹-cong   : Congruent₁ _⁻¹
+
+  open IsMonoid isMonoid public
+
+  inverseˡ : LeftInverse ε _⁻¹ _∙_
+  inverseˡ = proj₁ inverse
+
+  inverseʳ : RightInverse ε _⁻¹ _∙_
+  inverseʳ = proj₂ inverse
+
+  isInvertibleMagma : IsInvertibleMagma _∙_ ε _⁻¹
+  isInvertibleMagma = record
+    { isMagma = isMagma
+    ; inverse = inverse
+    ; ⁻¹-cong = ⁻¹-cong
+    }
+
+  isInvertibleUnitalMagma : IsInvertibleUnitalMagma _∙_ ε _⁻¹
+  isInvertibleUnitalMagma = record
+    { isInvertibleMagma = isInvertibleMagma
+    ; identity = identity
+    }
+
+  infixr 6 _\\_
+  _\\_ : Op₂ A
+  x \\ y = (x ⁻¹) ∙ y
+
+  infixl 6 _//_
+  _//_ : Op₂ A
+  x // y = x ∙ (y ⁻¹)
+
+  \\-cong₂ : Congruent₂ _\\_
+  \\-cong₂ x≈y u≈v = ∙-cong (⁻¹-cong x≈y) u≈v
+
+  //-cong₂ : Congruent₂ _//_
+  //-cong₂ x≈y u≈v = ∙-cong x≈y (⁻¹-cong u≈v)
+
+  open import Relation.Binary.Reasoning.Setoid setoid
+
+  \\-leftDividesˡ : LeftDividesˡ _∙_ _\\_
+  \\-leftDividesˡ x y = begin
+    x ∙ (x \\ y)  ≈⟨ assoc x (x ⁻¹) y ⟨
+    (x ∙ (x ⁻¹)) ∙ y   ≈⟨ ∙-congʳ (inverseʳ x) ⟩
+    ε ∙ y          ≈⟨ identityˡ y ⟩
+    y              ∎
+
+  \\-leftDividesʳ : LeftDividesʳ _∙_ _\\_
+  \\-leftDividesʳ x y = begin
+    x \\ (x ∙ y)     ≈⟨ assoc (x ⁻¹) x y ⟨
+    ((x ⁻¹) ∙ x) ∙ y   ≈⟨ ∙-congʳ (inverseˡ x) ⟩
+    ε ∙ y          ≈⟨ identityˡ y ⟩
+    y              ∎
+
+  \\-leftDivides : LeftDivides _∙_ _\\_
+  \\-leftDivides = \\-leftDividesˡ , \\-leftDividesʳ
+
+  //-rightDividesˡ : RightDividesˡ _∙_ _//_
+  //-rightDividesˡ x y = begin
+    (y // x) ∙ x    ≈⟨ assoc y (x ⁻¹) x ⟩
+    y ∙ ((x ⁻¹) ∙ x)  ≈⟨ ∙-congˡ (inverseˡ x) ⟩
+    y ∙ ε           ≈⟨ identityʳ y ⟩
+    y               ∎
+
+  //-rightDividesʳ : RightDividesʳ _∙_ _//_
+  //-rightDividesʳ x y = begin
+    y ∙ x // x    ≈⟨ assoc y x (x ⁻¹) ⟩
+    y ∙ (x // x)  ≈⟨ ∙-congˡ (inverseʳ x) ⟩
+    y ∙ ε         ≈⟨ identityʳ y ⟩
+    y             ∎
+
+  //-rightDivides : RightDivides _∙_ _//_
+  //-rightDivides = //-rightDividesˡ , //-rightDividesʳ
+
+  isQuasigroup : IsQuasigroup _∙_ _\\_ _//_
+  isQuasigroup = record
+    { isMagma = isMagma
+    ; \\-cong = \\-cong₂
+    ; //-cong = //-cong₂
+    ; leftDivides = \\-leftDivides
+    ; rightDivides = //-rightDivides
+    }
+
+  isLoop : IsLoop _∙_ _\\_ _//_ ε
+  isLoop = record { isQuasigroup = isQuasigroup ; 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)
diff --git a/src/Algebra/Structures/IsMagma.agda b/src/Algebra/Structures/IsMagma.agda
new file mode 100644
index 0000000000..75953d2235
--- /dev/null
+++ b/src/Algebra/Structures/IsMagma.agda
@@ -0,0 +1,148 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The `IsMagma` and related algebraic structures
+------------------------------------------------------------------------
+
+-- 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.IsMagma
+  {a ℓ} {A : Set a}  -- The underlying set
+  (_≈_ : Rel A ℓ)    -- The underlying equality relation
+  where
+
+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 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 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 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
+    }
diff --git a/src/Algebra/Structures/IsMonoid.agda b/src/Algebra/Structures/IsMonoid.agda
new file mode 100644
index 0000000000..1b55e743f1
--- /dev/null
+++ b/src/Algebra/Structures/IsMonoid.agda
@@ -0,0 +1,104 @@
+------------------------------------------------------------------------
+-- 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.IsMonoid
+  {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
+import Algebra.Properties.IsSemigroup as Properties
+open import Algebra.Structures.IsMagma _≈_
+open import Algebra.Structures.IsSemigroup _≈_
+open import Data.Product.Base using (_,_; proj₁; proj₂)
+open import Level using (_⊔_)
+
+------------------------------------------------------------------------
+-- Monoids
+------------------------------------------------------------------------
+
+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
+  open Properties isSemigroup public
+    using (isAlternativeMagma; isFlexibleMagma)
+
+  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
+  open Properties isSemigroup public
+    using (isAlternativeMagma; isFlexibleMagma)
+
+  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 }
diff --git a/src/Algebra/Structures/IsQuasigroup.agda b/src/Algebra/Structures/IsQuasigroup.agda
new file mode 100644
index 0000000000..9080382118
--- /dev/null
+++ b/src/Algebra/Structures/IsQuasigroup.agda
@@ -0,0 +1,107 @@
+------------------------------------------------------------------------
+-- 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)
+
+module Algebra.Structures.IsQuasigroup
+  {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 _≈_
+open import Algebra.Structures.IsMagma _≈_
+open import Data.Product.Base using (_,_; proj₁; proj₂)
+open import Level using (_⊔_)
+
+------------------------------------------------------------------------
+-- Quasigroups
+------------------------------------------------------------------------
+
+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
diff --git a/src/Algebra/Structures/IsSemigroup.agda b/src/Algebra/Structures/IsSemigroup.agda
new file mode 100644
index 0000000000..6094b0081d
--- /dev/null
+++ b/src/Algebra/Structures/IsSemigroup.agda
@@ -0,0 +1,76 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The `IsSemigroup` and related algebraic structures
+------------------------------------------------------------------------
+
+-- 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.IsSemigroup
+  {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 Algebra.Structures.IsMagma _≈_
+open import Data.Product.Base using (_,_; proj₁; proj₂)
+open import Level using (_⊔_)
+
+------------------------------------------------------------------------
+-- Semigroups
+------------------------------------------------------------------------
+
+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)
diff --git a/src/Algebra/Structures/IsSuccessorSet.agda b/src/Algebra/Structures/IsSuccessorSet.agda
new file mode 100644
index 0000000000..66f267b415
--- /dev/null
+++ b/src/Algebra/Structures/IsSuccessorSet.agda
@@ -0,0 +1,33 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The structure of a SuccessorSet
+------------------------------------------------------------------------
+
+-- 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.IsSuccessorSet
+  {a ℓ} {A : Set a}  -- The underlying set
+  (_≈_ : Rel A ℓ)    -- The underlying equality relation
+  where
+
+open import Algebra.Core using (Op₁)
+open import Algebra.Definitions _≈_
+open import Level using (_⊔_)
+
+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 }