diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0317a71b374ccfd093ffc29437fb6f530b23fc91..0c19f8792b17a0332b0967710a50f8a92db5c7fb 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -57,6 +57,8 @@ Coq 8.11 is no longer supported in this version of Iris.
 **Changes in `bi`:**
 
 * Add lemmas characterizing big-ops over pure predicates (`big_sep*_pure*`).
+* Move `BiAffine`, `BiPositive`, `BiLöb`, and `BiPureForall` from
+  `bi.derived_connectives` to `bi.extensions`.
 
 **Changes in `base_logic`:**
 
diff --git a/_CoqProject b/_CoqProject
index 21b032e94dc570f5da50005d910846a7a592e219..1ec0701913dc1725f179a23a79c9f1da5999b321 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -58,6 +58,7 @@ iris/si_logic/bi.v
 iris/bi/notation.v
 iris/bi/interface.v
 iris/bi/derived_connectives.v
+iris/bi/extensions.v
 iris/bi/derived_laws.v
 iris/bi/derived_laws_later.v
 iris/bi/plainly.v
diff --git a/iris/base_logic/bi.v b/iris/base_logic/bi.v
index 77be327e62d43d67c5125e9e81b8c4830b5f6489..f555ec33515d1dbc2a3cfe96686d08e269797805 100644
--- a/iris/base_logic/bi.v
+++ b/iris/base_logic/bi.v
@@ -1,4 +1,4 @@
-From iris.bi Require Export derived_connectives updates internal_eq plainly.
+From iris.bi Require Export derived_connectives extensions updates internal_eq plainly.
 From iris.base_logic Require Export upred.
 From iris.prelude Require Import options.
 Import uPred_primitive.
diff --git a/iris/bi/derived_connectives.v b/iris/bi/derived_connectives.v
index 7f965854e1f601170fe9466928ab295fb8af51b8..a5071e78a2bf2c2a7ce61c964ce90f8c87d8695f 100644
--- a/iris/bi/derived_connectives.v
+++ b/iris/bi/derived_connectives.v
@@ -30,14 +30,6 @@ Global Arguments Affine {_} _%I : simpl never.
 Global Arguments affine {_} _%I {_}.
 Global Hint Mode Affine + ! : typeclass_instances.
 
-Class BiAffine (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
-Global Hint Mode BiAffine ! : typeclass_instances.
-Global Existing Instance absorbing_bi | 0.
-
-Class BiPositive (PROP : bi) :=
-  bi_positive (P Q : PROP) : <affine> (P ∗ Q) ⊢ <affine> P ∗ Q.
-Global Hint Mode BiPositive ! : typeclass_instances.
-
 Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := True ∗ P.
 Global Arguments bi_absorbingly {_} _%I : simpl never.
 Global Instance: Params (@bi_absorbingly) 1 := {}.
@@ -117,28 +109,3 @@ Definition bi_wandM {PROP : bi} (mP : option PROP) (Q : PROP) : PROP :=
 Global Arguments bi_wandM {_} !_%I _%I /.
 Notation "mP -∗? Q" := (bi_wandM mP Q)
   (at level 99, Q at level 200, right associativity) : bi_scope.
-
-(** The class [BiLöb] is required for the [iLöb] tactic. However, for most BI
-logics [BiLaterContractive] should be used, which gives an instance of [BiLöb]
-automatically (see [derived_laws_later]). A direct instance of [BiLöb] is useful
-when considering a BI logic with a discrete OFE, instead of an OFE that takes
-step-indexing of the logic in account.
-
-The internal/"strong" version of Löb [(▷ P → P) ⊢ P] is derivable from [BiLöb].
-It is provided by the lemma [löb] in [derived_laws_later]. *)
-Class BiLöb (PROP : bi) :=
-  löb_weak (P : PROP) : (▷ P ⊢ P) → (True ⊢ P).
-Global Hint Mode BiLöb ! : typeclass_instances.
-Global Arguments löb_weak {_ _} _ _.
-
-Notation BiLaterContractive PROP :=
-  (Contractive (bi_later (PROP:=PROP))) (only parsing).
-
-(** The class [BiPureForall] states that universal quantification commutes with
-the embedding of pure propositions. The reverse direction of the entailment
-described by this type class is derivable, so it is not included.
-
-An instance of [BiPureForall] itself is derivable if we assume excluded middle
-in Coq, see the lemma [bi_pure_forall_em] in [derived_laws]. *)
-Class BiPureForall (PROP : bi) :=
-  pure_forall_2 : ∀ {A} (φ : A → Prop), (∀ a, ⌜ φ a ⌝) ⊢@{PROP} ⌜ ∀ a, φ a ⌝.
diff --git a/iris/bi/derived_laws.v b/iris/bi/derived_laws.v
index d5713f5cffc13366bf36c6ad52e77cd5e8ecd9af..fc8d8955d81f718756e12612ae27000e08bd65ad 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Import monoid.
-From iris.bi Require Export derived_connectives.
+From iris.bi Require Export extensions.
 From iris.prelude Require Import options.
 
 (* The sections add [BiAffine] and the like, which is only picked up with [Type*]. *)
diff --git a/iris/bi/extensions.v b/iris/bi/extensions.v
new file mode 100644
index 0000000000000000000000000000000000000000..6764ebe25c2423d5804a3e9c2810b06ecda8bca5
--- /dev/null
+++ b/iris/bi/extensions.v
@@ -0,0 +1,38 @@
+(** This file defines various extensions to the base BI interface, via
+typeclasses that BIs can optionally implement. *)
+
+From iris.bi Require Export derived_connectives.
+From iris.prelude Require Import options.
+
+Class BiAffine (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
+Global Hint Mode BiAffine ! : typeclass_instances.
+Global Existing Instance absorbing_bi | 0.
+
+Class BiPositive (PROP : bi) :=
+  bi_positive (P Q : PROP) : <affine> (P ∗ Q) ⊢ <affine> P ∗ Q.
+Global Hint Mode BiPositive ! : typeclass_instances.
+
+(** The class [BiLöb] is required for the [iLöb] tactic. However, for most BI
+logics [BiLaterContractive] should be used, which gives an instance of [BiLöb]
+automatically (see [derived_laws_later]). A direct instance of [BiLöb] is useful
+when considering a BI logic with a discrete OFE, instead of an OFE that takes
+step-indexing of the logic in account.
+
+The internal/"strong" version of Löb [(▷ P → P) ⊢ P] is derivable from [BiLöb].
+It is provided by the lemma [löb] in [derived_laws_later]. *)
+Class BiLöb (PROP : bi) :=
+  löb_weak (P : PROP) : (▷ P ⊢ P) → (True ⊢ P).
+Global Hint Mode BiLöb ! : typeclass_instances.
+Global Arguments löb_weak {_ _} _ _.
+
+Notation BiLaterContractive PROP :=
+  (Contractive (bi_later (PROP:=PROP))) (only parsing).
+
+(** The class [BiPureForall] states that universal quantification commutes with
+the embedding of pure propositions. The reverse direction of the entailment
+described by this type class is derivable, so it is not included.
+
+An instance of [BiPureForall] itself is derivable if we assume excluded middle
+in Coq, see the lemma [bi_pure_forall_em] in [derived_laws]. *)
+Class BiPureForall (PROP : bi) :=
+  pure_forall_2 : ∀ {A} (φ : A → Prop), (∀ a, ⌜ φ a ⌝) ⊢@{PROP} ⌜ ∀ a, φ a ⌝.