diff --git a/CHANGELOG.md b/CHANGELOG.md
index 225b699338..76e6a12c76 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -58,6 +58,11 @@ Deprecated names
   ∤∤-respˡ-≈    ↦  ∦-respˡ-≈
   ∤∤-respʳ-≈    ↦  ∦-respʳ-≈
   ∤∤-resp-≈     ↦  ∦-resp-≈
+  ∣-respʳ-≈    ↦ ∣ʳ-respʳ-≈
+  ∣-respˡ-≈    ↦ ∣ʳ-respˡ-≈
+  ∣-resp-≈     ↦ ∣ʳ-resp-≈
+  x∣yx         ↦ x∣ʳyx
+  xy≈z⇒y∣z     ↦ xy≈z⇒y∣ʳz
   ```
 
 * In `Algebra.Properties.Monoid.Divisibility`:
@@ -65,11 +70,17 @@ Deprecated names
   ∣∣-refl            ↦  ∥-refl
   ∣∣-reflexive       ↦  ∥-reflexive
   ∣∣-isEquivalence   ↦  ∥-isEquivalence
+  ε∣_                ↦ ε∣ʳ_
+  ∣-refl             ↦ ∣ʳ-refl
+  ∣-reflexive        ↦ ∣ʳ-reflexive
+  ∣-isPreorder       ↦ ∣ʳ-isPreorder
+  ∣-preorder         ↦ ∣ʳ-preorder
   ```
 
 * In `Algebra.Properties.Semigroup.Divisibility`:
   ```agda
   ∣∣-trans   ↦  ∥-trans
+  ∣-trans    ↦  ∣ʳ-trans
   ```
 
 * In `Data.List.Base`:
@@ -103,6 +114,10 @@ New modules
 
 * `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction` and `Data.Nat.ListAction.Properties`.
 
+* `Data.List.Relation.Binary.Prefix.Propositional.Properties` showing the equivalence to left divisibility induced by the list monoid.
+
+* `Data.List.Relation.Binary.Suffix.Propositional.Properties` showing the equivalence to right divisibility induced by the list monoid.
+
 * `Data.Sign.Show` to show a sign
 
 Additions to existing modules
@@ -137,6 +152,38 @@ Additions to existing modules
   commutativeRing                 : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ)
   ```
 
+* In `Algebra.Properties.Magma.Divisibility`:
+  ```agda
+  ∣ˡ-respʳ-≈  : _∣ˡ_ Respectsʳ _≈_
+  ∣ˡ-respˡ-≈  : _∣ˡ_ Respectsˡ _≈_
+  ∣ˡ-resp-≈   : _∣ˡ_ Respects₂ _≈_
+  x∣ˡxy       : ∀ x y → x ∣ˡ x ∙ y
+  xy≈z⇒x∣ˡz   : ∀ x y {z} → x ∙ y ≈ z → x ∣ˡ z
+  ```
+
+* In `Algebra.Properties.Monoid.Divisibility`:
+  ```agda
+  ε∣ˡ_          : ∀ x → ε ∣ˡ x
+  ∣ˡ-refl       : Reflexive _∣ˡ_
+  ∣ˡ-reflexive  : _≈_ ⇒ _∣ˡ_
+  ∣ˡ-isPreorder : IsPreorder _≈_ _∣ˡ_
+  ∣ˡ-preorder   : Preorder a ℓ _
+  ```
+
+* In `Algebra.Properties.Semigroup.Divisibility`:
+  ```agda
+  ∣ˡ-trans     : Transitive _∣ˡ_
+  x∣ʳy⇒x∣ʳzy   : x ∣ʳ y → x ∣ʳ z ∙ y
+  x∣ʳy⇒xz∣ʳyz  : x ∣ʳ y → x ∙ z ∣ʳ y ∙ z
+  x∣ˡy⇒zx∣ˡzy  : x ∣ˡ y → z ∙ x ∣ˡ z ∙ y
+  x∣ˡy⇒x∣ˡyz   : x ∣ˡ y → x ∣ˡ y ∙ z
+  ```
+
+* In `Algebra.Properties.CommutativeSemigroup.Divisibility`:
+  ```agda
+  ∙-cong-∣ : x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b
+  ```
+
 * In `Data.List.Properties`:
   ```agda
   map-applyUpTo : ∀ (f : ℕ → A) (g : A → B) n → map g (applyUpTo f n) ≡ applyUpTo (g ∘ f) n
@@ -149,3 +196,9 @@ Additions to existing modules
   ```agda
   filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys
   ```
+
+* In `Relation.Nullary.Decidable.Core`:
+  ```agda
+  ⊤-dec : Dec {a} ⊤
+  ⊥-dec : Dec {a} ⊥
+  ```
diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda
index 6532715a21..9667e33cc6 100644
--- a/src/Function/Bundles.agda
+++ b/src/Function/Bundles.agda
@@ -26,8 +26,7 @@ open import Level using (Level; _⊔_; suc)
 open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Core using (_Preserves_⟶_)
-open import Relation.Binary.PropositionalEquality.Core as ≡
-  using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as ≡
 open import Function.Consequences.Propositional
 open Setoid using (isEquivalence)
diff --git a/src/Function/Nary/NonDependent.agda b/src/Function/Nary/NonDependent.agda
index b1962a68c4..0d23bd0cbb 100644
--- a/src/Function/Nary/NonDependent.agda
+++ b/src/Function/Nary/NonDependent.agda
@@ -22,8 +22,7 @@ open import Data.Product.Nary.NonDependent
   using (Product; uncurryₙ; Equalₙ; curryₙ; fromEqualₙ; toEqualₙ)
 open import Function.Base using (_∘′_; _$′_; const; flip)
 open import Relation.Unary using (IUniversal)
-open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; cong)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
 
 private
   variable
diff --git a/src/Function/Nary/NonDependent/Base.agda b/src/Function/Nary/NonDependent/Base.agda
index 2f7347cdab..26a2ca61b7 100644
--- a/src/Function/Nary/NonDependent/Base.agda
+++ b/src/Function/Nary/NonDependent/Base.agda
@@ -17,7 +17,7 @@ module Function.Nary.NonDependent.Base where
 open import Level using (Level; 0ℓ; _⊔_)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Product.Base using (_×_; _,_)
-open import Data.Unit.Polymorphic.Base
+open import Data.Unit.Polymorphic.Base using (⊤; tt)
 open import Function.Base using (_∘′_; _$′_; const; flip)
 
 private
diff --git a/src/Function/Properties.agda b/src/Function/Properties.agda
index 08692108bc..bddb573e46 100644
--- a/src/Function/Properties.agda
+++ b/src/Function/Properties.agda
@@ -11,7 +11,7 @@ module Function.Properties where
 open import Axiom.Extensionality.Propositional using (Extensionality)
 open import Function.Base using (flip; _∘_)
 open import Function.Bundles using (_↔_; mk↔ₛ′; Inverse)
-open import Level
+open import Level using (Level)
 open import Relation.Binary.PropositionalEquality.Core
   using (trans; cong; cong′)
 
diff --git a/src/Function/Properties/Bijection.agda b/src/Function/Properties/Bijection.agda
index 21e295e807..c606ad5645 100644
--- a/src/Function/Properties/Bijection.agda
+++ b/src/Function/Properties/Bijection.agda
@@ -8,8 +8,8 @@
 
 module Function.Properties.Bijection where
 
-open import Function.Bundles using (Bijection; Inverse; Equivalence;
-  _⤖_; _↔_; _⇔_)
+open import Function.Bundles
+  using (Bijection; Inverse; Equivalence; _⤖_; _↔_; _⇔_)
 open import Level using (Level)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Structures using (IsEquivalence)
diff --git a/src/Function/Properties/Equivalence.agda b/src/Function/Properties/Equivalence.agda
index 5872569945..1ffe5fc561 100644
--- a/src/Function/Properties/Equivalence.agda
+++ b/src/Function/Properties/Equivalence.agda
@@ -9,9 +9,9 @@
 
 module Function.Properties.Equivalence where
 
-open import Function.Bundles
-open import Level
-open import Relation.Binary.Definitions
+open import Function.Bundles using (Func; Equivalence; _⇔_; _⟶_)
+open import Level using (Level; suc; _⊔_)
+open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive; Sym; Trans)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Structures using (IsEquivalence)
 import Relation.Binary.PropositionalEquality.Properties as ≡
diff --git a/src/Function/Properties/Injection.agda b/src/Function/Properties/Injection.agda
index b191513549..5963823fcd 100644
--- a/src/Function/Properties/Injection.agda
+++ b/src/Function/Properties/Injection.agda
@@ -8,11 +8,10 @@
 
 module Function.Properties.Injection where
 
-open import Function.Base
-open import Function.Definitions
-open import Function.Bundles
-import Function.Construct.Identity as Identity
-import Function.Construct.Composition as Compose
+open import Function.Definitions using (Injective)
+open import Function.Bundles using (Injection; Func; _⟶_; _↣_)
+import Function.Construct.Identity as Identity using (injection)
+import Function.Construct.Composition as Compose using (injection)
 open import Level using (Level)
 open import Data.Product.Base using (proj₁; proj₂)
 open import Relation.Binary.Definitions
diff --git a/src/Function/Properties/Inverse.agda b/src/Function/Properties/Inverse.agda
index 0579d70a62..c3d7d13490 100644
--- a/src/Function/Properties/Inverse.agda
+++ b/src/Function/Properties/Inverse.agda
@@ -11,15 +11,15 @@ module Function.Properties.Inverse where
 open import Axiom.Extensionality.Propositional using (Extensionality)
 open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Function.Bundles
-import Function.Properties.RightInverse as RightInverse
+import Function.Properties.RightInverse as RightInverse using (to-from)
 open import Level using (Level; _⊔_)
 open import Relation.Binary.Core using (REL)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Structures using (IsEquivalence)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
-import Relation.Binary.PropositionalEquality.Properties as ≡
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 import Function.Consequences.Setoid as Consequences
+  using (inverseʳ⇒injective; inverseˡ⇒surjective; inverseᵇ⇒bijective)
 
 import Function.Construct.Identity as Identity
 import Function.Construct.Symmetry as Symmetry
diff --git a/src/Function/Properties/Inverse/HalfAdjointEquivalence.agda b/src/Function/Properties/Inverse/HalfAdjointEquivalence.agda
index 05c20b9682..1fb4e36813 100644
--- a/src/Function/Properties/Inverse/HalfAdjointEquivalence.agda
+++ b/src/Function/Properties/Inverse/HalfAdjointEquivalence.agda
@@ -12,8 +12,8 @@ open import Function.Base using (id; _∘_)
 open import Function.Bundles using (Inverse; _↔_; mk↔ₛ′)
 open import Level using (Level; _⊔_)
 open import Relation.Binary.PropositionalEquality
-  using (_≡_; refl; cong; sym; trans; trans-reflʳ; cong-≡id; cong-∘; naturality;
-         cong-id; trans-assoc; trans-symˡ; module ≡-Reasoning)
+  using (_≡_; refl; cong; sym; trans; trans-reflʳ; cong-≡id; cong-∘; naturality
+        ; cong-id; trans-assoc; trans-symˡ; module ≡-Reasoning)
 
 private
   variable
diff --git a/src/Function/Properties/RightInverse.agda b/src/Function/Properties/RightInverse.agda
index ae8bc266de..43c6bba62b 100644
--- a/src/Function/Properties/RightInverse.agda
+++ b/src/Function/Properties/RightInverse.agda
@@ -8,8 +8,8 @@
 
 module Function.Properties.RightInverse where
 
-open import Function.Base
-open import Function.Definitions
+open import Function.Base using (id; _∘_)
+open import Function.Definitions using (Inverseˡ; Inverseʳ)
 open import Function.Bundles
 open import Function.Consequences using (inverseˡ⇒surjective)
 open import Level using (Level)
diff --git a/src/Function/Properties/Surjection.agda b/src/Function/Properties/Surjection.agda
index d5e6b8e75d..17b3dc657e 100644
--- a/src/Function/Properties/Surjection.agda
+++ b/src/Function/Properties/Surjection.agda
@@ -10,13 +10,13 @@ module Function.Properties.Surjection where
 
 open import Function.Base using (_∘_; _$_)
 open import Function.Definitions using (Surjective; Injective; Congruent)
-open import Function.Bundles using (Func; Surjection; _↠_; _⟶_; _↪_; mk↪;
-  _⇔_; mk⇔)
-import Function.Construct.Identity as Identity
-import Function.Construct.Composition as Compose
+open import Function.Bundles
+  using (Func; Surjection; _↠_; _⟶_; _↪_; mk↪; _⇔_; mk⇔)
+import Function.Construct.Identity as Identity using (surjection)
+import Function.Construct.Composition as Compose using (surjection)
 open import Level using (Level)
 open import Data.Product.Base using (proj₁; proj₂)
-import Relation.Binary.PropositionalEquality.Core as ≡
+import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl)
 open import Relation.Binary.Definitions using (Reflexive; Trans)
 open import Relation.Binary.Bundles using (Setoid)
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
diff --git a/src/Function/Related/Propositional.agda b/src/Function/Related/Propositional.agda
index 589c36a6b3..22d721e735 100644
--- a/src/Function/Related/Propositional.agda
+++ b/src/Function/Related/Propositional.agda
@@ -8,15 +8,16 @@
 
 module Function.Related.Propositional where
 
-open import Level
+open import Level using (Level; _⊔_)
 open import Relation.Binary
   using (Rel; REL; Sym; Reflexive; Trans; IsEquivalence; Setoid; IsPreorder; Preorder)
 open import Function.Bundles
-open import Function.Base
+  using (Func; Inverse; _⇔_; _↣_; _↠_; _↪_; _⟶_; _↔_; mk⟶; Equivalence; Injection
+        ; Surjection; RightInverse)
+open import Function.Base using (id; flip; _∘_; _∘′_; _$_)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as ≡
 open import Relation.Binary.Reasoning.Syntax
-
 open import Function.Properties.Surjection   using (↠⇒↪; ↠⇒⇔)
 open import Function.Properties.RightInverse using (↪⇒↠)
 open import Function.Properties.Bijection    using (⤖⇒↔; ⤖⇒⇔)
diff --git a/src/Function/Related/TypeIsomorphisms.agda b/src/Function/Related/TypeIsomorphisms.agda
index 478ef28a2e..79ec823836 100644
--- a/src/Function/Related/TypeIsomorphisms.agda
+++ b/src/Function/Related/TypeIsomorphisms.agda
@@ -9,7 +9,14 @@
 
 module Function.Related.TypeIsomorphisms where
 
-open import Algebra
+open import Algebra.Bundles public
+  using (Magma; Semigroup; Monoid; CommutativeMonoid; CommutativeSemiring)
+open import Algebra.Definitions
+  using (Identity; LeftIdentity; RightIdentity; Zero; LeftZero; RightZero
+        ; Associative; _DistributesOverˡ_; _DistributesOverʳ_; _DistributesOver_)
+open import Algebra.Structures public
+  using (IsMagma; IsSemigroup; IsMonoid; IsCommutativeMonoid
+        ; IsCommutativeSemiring)
 open import Algebra.Structures.Biased using (isCommutativeSemiringˡ)
 open import Axiom.Extensionality.Propositional using (Extensionality)
 open import Data.Bool.Base using (true; false)
@@ -360,3 +367,4 @@ True↔ (false because ofⁿ ¬p) _ =
 ∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y)
 ∃-≡ P {x} = mk↔ₛ′ (λ Px → x , refl , Px) (λ where (_ , refl , Py) → Py)
   (λ where (_ , refl , _) → refl) (λ where _ → refl)
+
diff --git a/src/Function/Related/TypeIsomorphisms/Solver.agda b/src/Function/Related/TypeIsomorphisms/Solver.agda
index 2d952ba82a..043ab70e7e 100644
--- a/src/Function/Related/TypeIsomorphisms/Solver.agda
+++ b/src/Function/Related/TypeIsomorphisms/Solver.agda
@@ -12,6 +12,7 @@ module Function.Related.TypeIsomorphisms.Solver where
 
 open import Algebra using (CommutativeSemiring)
 import Algebra.Solver.Ring.NaturalCoefficients.Default
+  using (solve; con; _:*_; _:+_; _:=_)
 open import Data.Empty.Polymorphic using (⊥)
 open import Data.Product.Base using (_×_)
 open import Data.Sum.Base using (_⊎_)
@@ -20,7 +21,7 @@ open import Level using (Level)
 open import Function.Bundles using (_↔_)
 open import Function.Properties.Inverse using (↔-refl)
 open import Function.Related.Propositional as Related
-open import Function.Related.TypeIsomorphisms
+open import Function.Related.TypeIsomorphisms using (×-⊎-commutativeSemiring)
 
 ------------------------------------------------------------------------
 -- The solver
diff --git a/src/Function/Structures/Biased.agda b/src/Function/Structures/Biased.agda
index e25c4970c9..8e570f2618 100644
--- a/src/Function/Structures/Biased.agda
+++ b/src/Function/Structures/Biased.agda
@@ -10,8 +10,7 @@
 {-# 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 Function.Structures.Biased {a b ℓ₁ ℓ₂}
   {A : Set a} (_≈₁_ : Rel A ℓ₁) -- Equality over the domain
@@ -19,11 +18,16 @@ module Function.Structures.Biased {a b ℓ₁ ℓ₂}
   where
 
 open import Data.Product.Base as Product using (∃; _×_; _,_)
-open import Function.Base
-open import Function.Definitions
-open import Function.Structures _≈₁_ _≈₂_
+open import Function.Base using (_∘_; id)
+open import Function.Definitions using(StrictlySurjective; StrictlyInverseˡ; StrictlyInverseʳ; Congruent)
 open import Function.Consequences.Setoid
+  using (strictlySurjective⇒surjective; strictlyInverseˡ⇒inverseˡ
+        ; strictlyInverseʳ⇒inverseʳ)
 open import Level using (_⊔_)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Structures using (IsEquivalence)
+
+open import Function.Structures _≈₁_ _≈₂_
 
 ------------------------------------------------------------------------
 -- Surjection