diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0cdb36f8c6..5dee17fe99 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1587,6 +1587,13 @@ Other minor changes
   moufangLoop : MoufangLoop a ℓ₁ → MoufangLoop b ℓ₂ → MoufangLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
  ```
 
+* Added new proofs to `Algebra.Construct.Flip.Op`:
+  ```agda
+  zero : Zero ≈ ε ∙ → Zero ≈ ε (flip ∙)
+  distributes : (≈ DistributesOver ∙) + → (≈ DistributesOver (flip ∙)) +
+  isRing : IsRing ≈ + * - 0# 1# → IsRing ≈ + (flip *) - 0# 1#
+  ```
+
 * Added new definition to `Algebra.Definitions`:
   ```agda
   LeftDividesˡ  : Op₂ A → Op₂ A → Set _
diff --git a/src/Algebra/Construct/Flip/Op.agda b/src/Algebra/Construct/Flip/Op.agda
index 471722cbd4..87c03301ab 100644
--- a/src/Algebra/Construct/Flip/Op.agda
+++ b/src/Algebra/Construct/Flip/Op.agda
@@ -9,7 +9,10 @@
 
 module Algebra.Construct.Flip.Op where
 
-open import Algebra
+open import Algebra.Core
+open import Algebra.Bundles
+import Algebra.Definitions as Def
+import Algebra.Structures as Str
 import Data.Product as Prod
 import Data.Sum as Sum
 open import Function.Base using (flip)
@@ -33,136 +36,171 @@ preserves₂ : (∼ ≈ ≋ : Rel A ℓ) →
              ∙ Preserves₂ ∼ ⟶ ≈ ⟶ ≋ → (flip ∙) Preserves₂ ≈ ⟶ ∼ ⟶ ≋
 preserves₂ _ _ _ pres = flip pres
 
-module _ (≈ : Rel A ℓ) (∙ : Op₂ A) where
+module ∙-Properties (≈ : Rel A ℓ) (∙ : Op₂ A) where
 
-  associative : Symmetric ≈ → Associative ≈ ∙ → Associative ≈ (flip ∙)
+  open Def ≈
+
+  associative : Symmetric ≈ → Associative ∙ → Associative (flip ∙)
   associative sym assoc x y z = sym (assoc z y x)
 
-  identity : Identity ≈ ε ∙ → Identity ≈ ε (flip ∙)
+  identity : Identity ε ∙ → Identity ε (flip ∙)
   identity id = Prod.swap id
 
-  commutative : Commutative ≈ ∙ → Commutative ≈ (flip ∙)
+  commutative : Commutative ∙ → Commutative (flip ∙)
   commutative comm = flip comm
 
-  selective : Selective ≈ ∙ → Selective ≈ (flip ∙)
+  selective : Selective ∙ → Selective (flip ∙)
   selective sel x y = Sum.swap (sel y x)
 
-  idempotent : Idempotent ≈ ∙ → Idempotent ≈ (flip ∙)
+  idempotent : Idempotent ∙ → Idempotent (flip ∙)
   idempotent idem = idem
 
-  inverse : Inverse ≈ ε ⁻¹ ∙ → Inverse ≈ ε ⁻¹ (flip ∙)
+  inverse : Inverse ε ⁻¹ ∙ → Inverse ε ⁻¹ (flip ∙)
   inverse inv = Prod.swap inv
 
+  zero : Zero ε ∙ → Zero ε (flip ∙)
+  zero zer = Prod.swap zer
+
+module *-Properties (≈ : Rel A ℓ) (* + : Op₂ A) where
+
+  open Def ≈
+
+  distributes : * DistributesOver + → (flip *) DistributesOver +
+  distributes distrib = Prod.swap distrib
+
 ------------------------------------------------------------------------
 -- Structures
 
 module _ {≈ : Rel A ℓ} {∙ : Op₂ A} where
 
-  isMagma : IsMagma ≈ ∙ → IsMagma ≈ (flip ∙)
+  open Def ≈
+  open Str ≈
+  open ∙-Properties ≈ ∙
+
+  isMagma : IsMagma ∙ → IsMagma (flip ∙)
   isMagma m = record
     { isEquivalence = isEquivalence
     ; ∙-cong        = preserves₂ ≈ ≈ ≈ ∙-cong
     }
     where open IsMagma m
 
-  isSelectiveMagma : IsSelectiveMagma ≈ ∙ → IsSelectiveMagma ≈ (flip ∙)
+  isSelectiveMagma : IsSelectiveMagma ∙ → IsSelectiveMagma (flip ∙)
   isSelectiveMagma m = record
     { isMagma = isMagma m.isMagma
-    ; sel     = selective ≈ ∙ m.sel
+    ; sel     = selective m.sel
     }
     where module m = IsSelectiveMagma m
 
-  isCommutativeMagma : IsCommutativeMagma ≈ ∙ → IsCommutativeMagma ≈ (flip ∙)
+  isCommutativeMagma : IsCommutativeMagma ∙ → IsCommutativeMagma (flip ∙)
   isCommutativeMagma m = record
     { isMagma = isMagma m.isMagma
-    ; comm    = commutative ≈ ∙ m.comm
+    ; comm    = commutative m.comm
     }
     where module m = IsCommutativeMagma m
 
-  isSemigroup : IsSemigroup ≈ ∙ → IsSemigroup ≈ (flip ∙)
+  isSemigroup : IsSemigroup ∙ → IsSemigroup (flip ∙)
   isSemigroup s = record
     { isMagma = isMagma s.isMagma
-    ; assoc   = associative ≈ ∙ s.sym s.assoc
+    ; assoc   = associative s.sym s.assoc
     }
     where module s = IsSemigroup s
 
-  isBand : IsBand ≈ ∙ → IsBand ≈ (flip ∙)
+  isBand : IsBand ∙ → IsBand (flip ∙)
   isBand b = record
     { isSemigroup = isSemigroup b.isSemigroup
     ; idem        = b.idem
     }
     where module b = IsBand b
 
-  isCommutativeSemigroup : IsCommutativeSemigroup ≈ ∙ →
-                           IsCommutativeSemigroup ≈ (flip ∙)
+  isCommutativeSemigroup : IsCommutativeSemigroup ∙ →
+                           IsCommutativeSemigroup (flip ∙)
   isCommutativeSemigroup s = record
     { isSemigroup = isSemigroup s.isSemigroup
-    ; comm        = commutative ≈ ∙ s.comm
+    ; comm        = commutative s.comm
     }
     where module s = IsCommutativeSemigroup s
 
-  isUnitalMagma : IsUnitalMagma ≈ ∙ ε → IsUnitalMagma ≈ (flip ∙) ε
+  isUnitalMagma : IsUnitalMagma ∙ ε → IsUnitalMagma (flip ∙) ε
   isUnitalMagma m = record
     { isMagma  = isMagma m.isMagma
-    ; identity = identity ≈ ∙ m.identity
+    ; identity = identity m.identity
     }
     where module m = IsUnitalMagma m
 
-  isMonoid : IsMonoid ≈ ∙ ε → IsMonoid ≈ (flip ∙) ε
+  isMonoid : IsMonoid ∙ ε → IsMonoid (flip ∙) ε
   isMonoid m = record
     { isSemigroup = isSemigroup m.isSemigroup
-    ; identity    = identity ≈ ∙ m.identity
+    ; identity    = identity m.identity
     }
     where module m = IsMonoid m
 
-  isCommutativeMonoid : IsCommutativeMonoid ≈ ∙ ε →
-                        IsCommutativeMonoid ≈ (flip ∙) ε
+  isCommutativeMonoid : IsCommutativeMonoid ∙ ε →
+                        IsCommutativeMonoid (flip ∙) ε
   isCommutativeMonoid m = record
     { isMonoid = isMonoid m.isMonoid
-    ; comm     = commutative ≈ ∙ m.comm
+    ; comm     = commutative m.comm
     }
     where module m = IsCommutativeMonoid m
 
-  isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid ≈ ∙ ε →
-                                  IsIdempotentCommutativeMonoid ≈ (flip ∙) ε
+  isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid ∙ ε →
+                                  IsIdempotentCommutativeMonoid (flip ∙) ε
   isIdempotentCommutativeMonoid m = record
     { isCommutativeMonoid = isCommutativeMonoid m.isCommutativeMonoid
-    ; idem                = idempotent ≈ ∙ m.idem
+    ; idem                = idempotent m.idem
     }
     where module m = IsIdempotentCommutativeMonoid m
 
-  isInvertibleMagma : IsInvertibleMagma ≈ ∙ ε ⁻¹ →
-                      IsInvertibleMagma ≈ (flip ∙) ε ⁻¹
+  isInvertibleMagma : IsInvertibleMagma ∙ ε ⁻¹ →
+                      IsInvertibleMagma (flip ∙) ε ⁻¹
   isInvertibleMagma m = record
     { isMagma = isMagma m.isMagma
-    ; inverse = inverse ≈ ∙ m.inverse
+    ; inverse = inverse m.inverse
     ; ⁻¹-cong = m.⁻¹-cong
     }
     where module m = IsInvertibleMagma m
 
-  isInvertibleUnitalMagma : IsInvertibleUnitalMagma ≈ ∙ ε ⁻¹ →
-                            IsInvertibleUnitalMagma ≈ (flip ∙) ε ⁻¹
+  isInvertibleUnitalMagma : IsInvertibleUnitalMagma ∙ ε ⁻¹ →
+                            IsInvertibleUnitalMagma (flip ∙) ε ⁻¹
   isInvertibleUnitalMagma m = record
     { isInvertibleMagma = isInvertibleMagma m.isInvertibleMagma
-    ; identity          = identity ≈ ∙ m.identity
+    ; identity          = identity m.identity
     }
     where module m = IsInvertibleUnitalMagma m
 
-  isGroup : IsGroup ≈ ∙ ε ⁻¹ → IsGroup ≈ (flip ∙) ε ⁻¹
+  isGroup : IsGroup ∙ ε ⁻¹ → IsGroup (flip ∙) ε ⁻¹
   isGroup g = record
     { isMonoid = isMonoid g.isMonoid
-    ; inverse  = inverse ≈ ∙ g.inverse
+    ; inverse  = inverse g.inverse
     ; ⁻¹-cong  = g.⁻¹-cong
     }
     where module g = IsGroup g
 
-  isAbelianGroup : IsAbelianGroup ≈ ∙ ε ⁻¹ → IsAbelianGroup ≈ (flip ∙) ε ⁻¹
+  isAbelianGroup : IsAbelianGroup ∙ ε ⁻¹ → IsAbelianGroup (flip ∙) ε ⁻¹
   isAbelianGroup g = record
     { isGroup = isGroup g.isGroup
-    ; comm    = commutative ≈ ∙ g.comm
+    ; comm    = commutative g.comm
     }
     where module g = IsAbelianGroup g
 
+module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# 1# : A} where
+
+  open Str ≈
+  open ∙-Properties ≈ *
+  open *-Properties ≈ * +
+
+  isRing : IsRing + * - 0# 1# → IsRing + (flip *) - 0# 1#
+  isRing r = record
+    { +-isAbelianGroup = r.+-isAbelianGroup
+    ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong
+    ; *-assoc = associative r.sym r.*-assoc
+    ; *-identity = identity r.*-identity
+    ; distrib = distributes r.distrib
+    ; zero = zero r.zero
+    }
+    where
+      module r = IsRing r
+
+
 ------------------------------------------------------------------------
 -- Bundles
 
@@ -239,3 +277,7 @@ group g = record { isGroup = isGroup g.isGroup }
 abelianGroup : AbelianGroup a ℓ → AbelianGroup a ℓ
 abelianGroup g = record { isAbelianGroup = isAbelianGroup g.isAbelianGroup }
   where module g = AbelianGroup g
+
+ring : Ring a ℓ → Ring a ℓ
+ring r = record { isRing = isRing r.isRing }
+  where module r = Ring r
diff --git a/src/Algebra/Construct/Initial.agda b/src/Algebra/Construct/Initial.agda
new file mode 100644
index 0000000000..14b1b32fef
--- /dev/null
+++ b/src/Algebra/Construct/Initial.agda
@@ -0,0 +1,97 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Instances of algebraic structures where the carrier is ⊥.
+-- In mathematics, this is usually called 0.
+--
+-- From monoids up, these are zero-objects – i.e, the initial
+-- object is the terminal object in the relevant category.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+
+module Algebra.Construct.Initial {c ℓ : Level} where
+
+open import Algebra.Bundles
+  using (Magma; Semigroup; Band)
+open import Algebra.Bundles.Raw
+  using (RawMagma)
+open import Algebra.Core using (Op₂)
+open import Algebra.Definitions using (Congruent₂)
+open import Algebra.Structures using (IsMagma; IsSemigroup; IsBand)
+open import Data.Empty.Polymorphic
+open import Relation.Binary using (Rel; Reflexive; Symmetric; Transitive; IsEquivalence)
+
+
+------------------------------------------------------------------------
+-- re-export those algebras which are also terminal
+
+open import Algebra.Construct.Terminal {c} {ℓ} public
+  hiding (rawMagma; magma; semigroup; band)
+
+------------------------------------------------------------------------
+-- gather all the functionality in one place
+
+private module ℤero where
+
+  infixl 7 _∙_
+  infix  4 _≈_
+
+  Carrier : Set c
+  Carrier = ⊥
+
+  _≈_     : Rel Carrier ℓ
+  _≈_ ()
+
+  _∙_     : Op₂ Carrier
+  _∙_ ()
+
+  refl : Reflexive _≈_
+  refl {x = ()}
+
+  sym : Symmetric _≈_
+  sym {x = ()}
+
+  trans : Transitive _≈_
+  trans {i = ()}
+
+  ∙-cong : Congruent₂ _≈_ _∙_
+  ∙-cong {x = ()}
+
+open ℤero
+
+------------------------------------------------------------------------
+-- Raw bundles
+
+rawMagma : RawMagma c ℓ
+rawMagma = record { Carrier = Carrier ; _≈_ = _≈_ ; _∙_ = _∙_ }
+
+------------------------------------------------------------------------
+-- Structures
+
+isEquivalence : IsEquivalence _≈_
+isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
+
+isMagma : IsMagma _≈_ _∙_
+isMagma = record { isEquivalence = isEquivalence ; ∙-cong = ∙-cong }
+
+isSemigroup : IsSemigroup _≈_ _∙_
+isSemigroup = record { isMagma = isMagma ; assoc = λ () }
+
+isBand : IsBand _≈_ _∙_
+isBand = record { isSemigroup = isSemigroup ; idem = λ () }
+
+------------------------------------------------------------------------
+-- Bundles
+
+magma : Magma c ℓ
+magma = record { isMagma = isMagma }
+
+semigroup : Semigroup c ℓ
+semigroup = record { isSemigroup = isSemigroup }
+
+band : Band c ℓ
+band = record { isBand = isBand }
+
diff --git a/src/Algebra/Construct/Terminal.agda b/src/Algebra/Construct/Terminal.agda
new file mode 100644
index 0000000000..b932710c57
--- /dev/null
+++ b/src/Algebra/Construct/Terminal.agda
@@ -0,0 +1,88 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Instances of algebraic structures where the carrier is ⊤.
+-- In mathematics, this is usually called 0 (1 in the case of Group).
+--
+-- From monoids up, these are zero-objects – i.e, both the initial
+-- and the terminal object in the relevant category.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+
+module Algebra.Construct.Terminal {c ℓ : Level} where
+
+open import Algebra.Bundles
+open import Data.Unit.Polymorphic
+open import Relation.Binary.Core using (Rel)
+
+------------------------------------------------------------------------
+-- Gather all the functionality in one place
+
+private module 𝕆ne where
+
+  infix  4 _≈_
+  Carrier : Set c
+  Carrier = ⊤
+  
+  _≈_     : Rel Carrier ℓ
+  _ ≈ _ = ⊤
+
+open 𝕆ne
+
+------------------------------------------------------------------------
+-- Raw bundles
+
+rawMagma : RawMagma c ℓ
+rawMagma = record { Carrier = Carrier ; _≈_ = _≈_ }
+
+rawMonoid : RawMonoid c ℓ
+rawMonoid = record { Carrier = Carrier ; _≈_ = _≈_ }
+
+rawGroup : RawGroup c ℓ
+rawGroup = record { Carrier = Carrier ; _≈_ = _≈_ }
+
+rawSemiring : RawSemiring c ℓ
+rawSemiring = record { Carrier = Carrier ; _≈_ = _≈_ }
+
+rawRing : RawRing c ℓ
+rawRing = record { Carrier = Carrier ; _≈_ = _≈_ }
+
+------------------------------------------------------------------------
+-- Bundles
+
+magma : Magma c ℓ
+magma = record { Carrier = Carrier ; _≈_ = _≈_ }
+
+semigroup : Semigroup c ℓ
+semigroup = record { Carrier = Carrier ; _≈_ = _≈_ }
+
+band : Band c ℓ
+band = record { Carrier = Carrier ; _≈_ = _≈_ }
+
+commutativeSemigroup : CommutativeSemigroup c ℓ
+commutativeSemigroup = record { Carrier = Carrier ; _≈_ = _≈_ }
+
+monoid : Monoid c ℓ
+monoid = record { Carrier = Carrier ; _≈_ = _≈_ }
+
+commutativeMonoid : CommutativeMonoid c ℓ
+commutativeMonoid = record { Carrier = Carrier ; _≈_ = _≈_ }
+
+idempotentCommutativeMonoid : IdempotentCommutativeMonoid c ℓ
+idempotentCommutativeMonoid = record { Carrier = Carrier ; _≈_ = _≈_ }
+
+group : Group c ℓ
+group = record { Carrier = Carrier ; _≈_ = _≈_ }
+
+abelianGroup : AbelianGroup c ℓ
+abelianGroup = record { Carrier = Carrier ; _≈_ = _≈_ }
+
+semiring : Semiring c ℓ
+semiring = record { Carrier = Carrier ; _≈_ = _≈_ }
+
+ring : Ring c ℓ
+ring = record { Carrier = Carrier ; _≈_ = _≈_ }
+
diff --git a/src/Algebra/Construct/Zero.agda b/src/Algebra/Construct/Zero.agda
index 12f5c87ffe..a608d2d686 100644
--- a/src/Algebra/Construct/Zero.agda
+++ b/src/Algebra/Construct/Zero.agda
@@ -18,10 +18,6 @@ open import Level using (Level)
 module Algebra.Construct.Zero {c ℓ : Level} where
 
 open import Algebra.Bundles
-open import Data.Unit.Polymorphic
-
-------------------------------------------------------------------------
--- Raw bundles
 
 rawMagma : RawMagma c ℓ
 rawMagma = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
@@ -32,9 +28,6 @@ rawMonoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
 rawGroup : RawGroup c ℓ
 rawGroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
 
-------------------------------------------------------------------------
--- Bundles
-
 magma : Magma c ℓ
 magma = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
 
diff --git a/src/Algebra/Module/Construct/Zero.agda b/src/Algebra/Module/Construct/Zero.agda
index ada60892c5..b6a1b2d637 100644
--- a/src/Algebra/Module/Construct/Zero.agda
+++ b/src/Algebra/Module/Construct/Zero.agda
@@ -17,56 +17,56 @@ module Algebra.Module.Construct.Zero {c ℓ : Level} where
 open import Algebra.Bundles
 open import Algebra.Module.Bundles
 open import Data.Unit.Polymorphic
+open import Relation.Binary.Core using (Rel)
 
 private
   variable
     r s ℓr ℓs : Level
 
+------------------------------------------------------------------------
+-- gather all the functionality in one place
+
+private module ℤero where
+
+  infix  4 _≈_
+  Carrier : Set c
+  _≈_     : Rel Carrier ℓ
+
+  Carrier = ⊤
+  _ ≈ _ = ⊤
+
+open ℤero
+
+------------------------------------------------------------------------
+-- Raw bundles NOT YET IMPLEMENTED issue #1828
+{-
+rawModule : RawModule c ℓ
+rawModule = record { Carrier = Carrier ; _≈_ = _≈_ }
+-}
+------------------------------------------------------------------------
+-- Bundles
+
 leftSemimodule : {R : Semiring r ℓr} → LeftSemimodule R c ℓ
-leftSemimodule = record
-  { Carrierᴹ = ⊤
-  ; _≈ᴹ_ = λ _ _ → ⊤
-  }
+leftSemimodule = record { Carrierᴹ = Carrier ; _≈ᴹ_ = _≈_ }
 
 rightSemimodule : {S : Semiring s ℓs} → RightSemimodule S c ℓ
-rightSemimodule = record
-  { Carrierᴹ = ⊤
-  ; _≈ᴹ_ = λ _ _ → ⊤
-  }
+rightSemimodule = record { Carrierᴹ = Carrier ; _≈ᴹ_ = _≈_ }
 
 bisemimodule :
   {R : Semiring r ℓr} {S : Semiring s ℓs} → Bisemimodule R S c ℓ
-bisemimodule = record
-  { Carrierᴹ = ⊤
-  ; _≈ᴹ_ = λ _ _ → ⊤
-  }
+bisemimodule = record { Carrierᴹ = Carrier ; _≈ᴹ_ = _≈_ }
 
 semimodule : {R : CommutativeSemiring r ℓr} → Semimodule R c ℓ
-semimodule = record
-  { Carrierᴹ = ⊤
-  ; _≈ᴹ_ = λ _ _ → ⊤
-  }
+semimodule = record { Carrierᴹ = Carrier ; _≈ᴹ_ = _≈_ }
 
 leftModule : {R : Ring r ℓr} → LeftModule R c ℓ
-leftModule = record
-  { Carrierᴹ = ⊤
-  ; _≈ᴹ_ = λ _ _ → ⊤
-  }
+leftModule = record { Carrierᴹ = Carrier ; _≈ᴹ_ = _≈_ }
 
 rightModule : {S : Ring s ℓs} → RightModule S c ℓ
-rightModule = record
-  { Carrierᴹ = ⊤
-  ; _≈ᴹ_ = λ _ _ → ⊤
-  }
+rightModule = record { Carrierᴹ = Carrier ; _≈ᴹ_ = _≈_ }
 
 bimodule : {R : Ring r ℓr} {S : Ring s ℓs} → Bimodule R S c ℓ
-bimodule = record
-  { Carrierᴹ = ⊤
-  ; _≈ᴹ_ = λ _ _ → ⊤
-  }
+bimodule = record { Carrierᴹ = Carrier ; _≈ᴹ_ = _≈_ }
 
 ⟨module⟩ : {R : CommutativeRing r ℓr} → Module R c ℓ
-⟨module⟩ = record
-  { Carrierᴹ = ⊤
-  ; _≈ᴹ_ = λ _ _ → ⊤
-  }
+⟨module⟩ = record { Carrierᴹ = Carrier ; _≈ᴹ_ = _≈_ }
diff --git a/src/Data/Unit.agda b/src/Data/Unit.agda
index fd03e9bcad..22a97b4af9 100644
--- a/src/Data/Unit.agda
+++ b/src/Data/Unit.agda
@@ -8,8 +8,6 @@
 
 module Data.Unit where
 
-import Relation.Binary.PropositionalEquality as PropEq
-
 ------------------------------------------------------------------------
 -- Re-export contents of base module
 
diff --git a/src/Data/Unit/Base.agda b/src/Data/Unit/Base.agda
index b30cd40d40..49ae91be88 100644
--- a/src/Data/Unit/Base.agda
+++ b/src/Data/Unit/Base.agda
@@ -6,8 +6,6 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-open import Agda.Builtin.Equality using (_≡_)
-
 module Data.Unit.Base where
 
 ------------------------------------------------------------------------